Theorem ExteriorAlgebra.basis_apply_ofCard

Modification history

2026-10-11 17:26

Mathlib/LinearAlgebra/ExteriorAlgebra/Basis.lean

chore: use the `Finset.card` notation more widely (#44638) …

Modified ExteriorAlgebra.basis_apply_ofCard View on Github →

2026-03-06 04:53

Mathlib/LinearAlgebra/ExteriorAlgebra/Basis.lean

feat(LinearAlgebra/ExteriorAlgebra): `Basis` for `ExteriorAlgebra` (#35424) …

Added ExteriorAlgebra.basis_apply_ofCard View on Github →