Code

MathComp 2.3 compat#15

Code

Merged

hivert merged 6 commits intomastermath-comp/Coq-Combi:masterfrom MC-2.3math-comp/Coq-Combi:MC-2.3Copy head branch name to clipboardJan 7, 2025

+534-957

Commits

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