Code

Bruhat#7

Code

Open

hivert wants to merge 22 commits intomastermath-comp/Coq-Combi:masterfrom Bruhatmath-comp/Coq-Combi:BruhatCopy head branch name to clipboard

+1,940-485

Commits

Commits on Feb 10, 2024

• WIP on Bruhat order

  hivert

  committed
  037871f

  Copy full SHA for 037871f

• Before big cleanup

  hivert

  committed
  99679ee

  Copy full SHA for 99679ee

• Characterization of permutation growth matrices

  hivert

  committed
  eea9d05

  Copy full SHA for eea9d05

• Better notations

  hivert

  committed
  0cb944e

  Copy full SHA for 0cb944e

• Proof of is_pmxsumP

  hivert

  committed
  4651176

  Copy full SHA for 4651176

• Added Bruhat to _CoqProject

  hivert

  committed
  48f678e

  Copy full SHA for 48f678e

• Minor proof improvements

  hivert

  committed
  49ec5ad

  Copy full SHA for 49ec5ad

• Documentation in Bruhat

  hivert

  committed
  df651ce

  Copy full SHA for df651ce

• Generalized n0.+1 -> n when possible

  hivert

  committed
  c81fc83

  Copy full SHA for c81fc83

• Bruhat Order Symmetry

  hivert

  committed
  9e6a263

  Copy full SHA for 9e6a263

• Minor cleanup

  hivert

  committed
  e3edd08

  Copy full SHA for e3edd08

Commits on Feb 11, 2024

• Used Order.NatMonotonyTheory.nondecn_inP

  hivert

  committed
  593ce92

  Copy full SHA for 593ce92

• Added #[local] + proof

  hivert

  committed
  626b3ec

  Copy full SHA for 626b3ec

Commits on Jan 3, 2025

• MathComp 2.3 compat

  hivert

  committed
  a3d2439

  Copy full SHA for a3d2439

• Nix for MathComp 2.3

  hivert

  committed
  fded742

  Copy full SHA for fded742

Commits on Jan 4, 2025

• Used bilinear maps from new MC 2.0 sesquilinear

  hivert

  committed
  3324d95

  Copy full SHA for 3324d95

Commits on Jan 5, 2025

• Orthogonal and orthonormal from sesquilinear

  hivert

  committed
  68bf88a

  Copy full SHA for 68bf88a

• Cosmetic

  hivert

  committed
  65e8e3c

  Copy full SHA for 65e8e3c

• Hermitian product on class function + isometry

  hivert

  committed
  049cc63

  Copy full SHA for 049cc63

Commits on Jan 7, 2025

• Version notes

  hivert

  committed
  c728d1d

  Copy full SHA for c728d1d

Commits on Jan 8, 2025

• Merge MC.2.3

  hivert

  committed
  7f6335c

  Copy full SHA for 7f6335c

• Fix the doc

  hivert

  committed
  030834c

  Copy full SHA for 030834c