Basis

📁 Source: Mathlib/LinearAlgebra/ExteriorAlgebra/Basis.lean

Statistics

Metric	Count
Definitions instDecompositionNatSubmoduleExteriorPower, ExteriorAlgebra	2
Theorems basis_apply, basis_apply_ofCard, basis_apply_powersetCard, basis_eq_coe_basis, basis_mul_of_disjoint, basis_mul_of_not_disjoint	6
Total	8

ExteriorAlgebra

Definitions

Name	Category	Theorems
instDecompositionNatSubmoduleExteriorPower 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Finset ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule Module.Basis.instFunLike Module.Basis.ExteriorAlgebra ιMulti_family Finset.card Set.Elem Set.powersetCard Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Set.powersetCard.prodEquiv	—	Module.Basis.coe_reindex DirectSum.IsInternal.collectedBasis_coe exteriorPower.coe_basis
basis_apply_ofCard 📖	mathematical	Finset.card	DFunLike.coe Module.Basis Finset ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule Module.Basis.instFunLike Module.Basis.ExteriorAlgebra ιMulti_family Set.powersetCard.ofCard	—	basis_apply
basis_apply_powersetCard 📖	mathematical	—	DFunLike.coe Module.Basis Finset ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule Module.Basis.instFunLike Module.Basis.ExteriorAlgebra Set Set.instMembership Set.powersetCard ιMulti_family	—	basis_apply_ofCard Set.powersetCard.card_eq
basis_eq_coe_basis 📖	mathematical	—	DFunLike.coe Module.Basis Finset ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule Module.Basis.instFunLike Module.Basis.ExteriorAlgebra Set Set.instMembership Set.powersetCard Submodule SetLike.instMembership Submodule.setLike exteriorPower Set.Elem Submodule.addCommMonoid Submodule.module Module.Basis.exteriorPower	—	basis_apply_powersetCard exteriorPower.basis_apply exteriorPower.ιMulti_family_apply_coe
basis_mul_of_disjoint 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot Set Set.instMembership Set.powersetCard	ExteriorAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule DFunLike.coe Module.Basis Finset CliffordAlgebra.instModule Module.Basis.instFunLike Module.Basis.ExteriorAlgebra Set Set.instMembership Set.powersetCard Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign Fin.fintype Set.powersetCard.permOfDisjoint Set.powersetCard.disjUnion	—	basis_apply_powersetCard ιMulti_family_mul_of_disjoint
basis_mul_of_not_disjoint 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot Set Set.instMembership Set.powersetCard	ExteriorAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule DFunLike.coe Module.Basis Finset CliffordAlgebra.instModule Module.Basis.instFunLike Module.Basis.ExteriorAlgebra Set Set.instMembership Set.powersetCard MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	basis_apply_powersetCard ιMulti_family_mul_of_not_disjoint

Module.Basis

Definitions

Name	Category	Theorems
ExteriorAlgebra 📖	CompOp	6 math math: ExteriorAlgebra.basis_mul_of_disjoint, ExteriorAlgebra.basis_eq_coe_basis, ExteriorAlgebra.basis_apply, ExteriorAlgebra.basis_apply_ofCard, ExteriorAlgebra.basis_apply_powersetCard, ExteriorAlgebra.basis_mul_of_not_disjoint

---

← Back to Index