Theorems · Definition · linear algebra
ExteriorAlgebra
(R : Type u1) → [inst : CommRing R] → (M : Type u2) → [inst_1 : AddCommGroup M] → [Module R M] → Type (max u1 u2)
The exterior algebra of an R-module M.
- Cited by
- 131 results in Mathlib
- Foundations
- Depth 41 from the axioms, rests on 508 definitions · uses propext, Quot.sound
- Assumes
- CommRingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- CliffordAlgebraproof · cited by 309
Cited by163
Results whose statement or proof uses this declaration.
- ExteriorAlgebra.exteriorPowerstatement · cited by 66
- ExteriorAlgebra.ιstatement · cited by 39
- exteriorPower.ιMultistatement · cited by 30
- ExteriorAlgebra.ιMultistatement and proof · cited by 26
- exteriorPower.ιMulti_familystatement · cited by 17
- exteriorPower.mapstatement · cited by 14
- ExteriorAlgebra.mapstatement · cited by 13
- Module.Basis.exteriorPowerstatement · cited by 12
- ModuleCat.exteriorPowerproof · cited by 12
- ExteriorAlgebra.liftAlternatingstatement and proof · cited by 9
- ExteriorAlgebra.ιMulti_familystatement · cited by 9
- exteriorPower.alternatingMapLinearEquiv_apply_ιMultistatement · cited by 8