Theorem ExteriorAlgebra.basis_mul_of_not_disjoint

Modification history

2026-03-06 04:53

Mathlib/LinearAlgebra/ExteriorAlgebra/Basis.lean

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

Added ExteriorAlgebra.basis_mul_of_not_disjoint View on Github →