Basis

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

Statistics

Metric	Count
Definitions exteriorPower, ιMultiDual	2
Theorems basis_apply, basis_coord, basis_repr, basis_repr_apply, basis_repr_ne, basis_repr_self, coe_basis, finrank_eq, instFinite, instFree, ιMultiDual_apply_diag, ιMultiDual_apply_nondiag, ιMultiDual_apply_ιMulti, ιMulti_family_linearIndependent_field, ιMulti_family_linearIndependent_ofBasis	15
Total	17

Module.Basis

Definitions

Name	Category	Theorems
exteriorPower 📖	CompOp	7 math math: exteriorPower.basis_apply, exteriorPower.coe_basis, exteriorPower.basis_repr_ne, exteriorPower.basis_coord, exteriorPower.basis_repr_apply, exteriorPower.basis_repr, exteriorPower.basis_repr_self

exteriorPower

Definitions

Name	Category	Theorems
ιMultiDual 📖	CompOp	5 math math: ιMultiDual_apply_diag, ιMultiDual_apply_ιMulti, basis_coord, basis_repr_apply, ιMultiDual_apply_nondiag

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Set.Elem Finset Set.powersetCard ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Module.Basis.instFunLike Module.Basis.exteriorPower ιMulti_family	—	coe_basis
basis_coord 📖	mathematical	—	Module.Basis.coord Set.Elem Finset Set.powersetCard ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Module.Basis.exteriorPower ιMultiDual	—	LinearMap.ext_on ιMulti_family_span_of_span Module.Basis.span_eq RingHomInvPair.ids Module.Basis.coord_apply ιMultiDual_apply_diag basis_apply Module.Basis.repr_self Finsupp.single_eq_same ιMultiDual_apply_nondiag Finsupp.single_eq_of_ne
basis_repr 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Finsupp Set.Elem Finset Set.powersetCard MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Submodule.addCommMonoid Finsupp.instAddCommMonoid Submodule.module Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Module.Basis.exteriorPower ιMulti_family Module.Basis Module.Basis.instFunLike Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Finsupp.ext RingHomInvPair.ids basis_repr_self Finsupp.single_eq_same basis_repr_ne Finsupp.single_eq_of_ne'
basis_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp Set.Elem Finset Set.powersetCard MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Finsupp.instAddCommMonoid Submodule.module Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Module.Basis.exteriorPower Module.Dual LinearMap.instFunLike ιMultiDual	—	RingHomInvPair.ids LinearMap.congr_fun basis_coord
basis_repr_ne 📖	mathematical	—	DFunLike.coe Finsupp Set.Elem Finset Set.powersetCard MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Finsupp.instAddCommMonoid Submodule.module Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Module.Basis.exteriorPower ιMulti_family Module.Basis Module.Basis.instFunLike NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids basis_repr_apply ιMultiDual_apply_nondiag
basis_repr_self 📖	mathematical	—	DFunLike.coe Finsupp Set.Elem Finset Set.powersetCard MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Finsupp.instAddCommMonoid Submodule.module Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Module.Basis.exteriorPower ιMulti_family Module.Basis Module.Basis.instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids basis_repr_apply ιMultiDual_apply_diag
coe_basis 📖	mathematical	—	DFunLike.coe Module.Basis Set.Elem Finset Set.powersetCard ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Module.Basis.instFunLike Module.Basis.exteriorPower ιMulti_family	—	ιMulti_family_linearIndependent_ofBasis
finrank_eq 📖	mathematical	—	Module.finrank ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Nat.choose	—	WellFoundedRelation.isWellFounded Module.finrank_eq_card_basis commRing_strongRankCondition Fintype.card_eq_nat_card Set.powersetCard.card
instFinite 📖	mathematical	—	Module.Finite ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module	—	Module.Finite.iff_fg ExteriorAlgebra.exteriorPower.eq_1 LinearMap.range_eq_map Submodule.FG.pow Submodule.FG.map Module.Finite.fg_top
instFree 📖	mathematical	—	Module.Free ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module	—	Module.Free.exists_basis Module.Free.of_basis WellFoundedRelation.isWellFounded
ιMultiDual_apply_diag 📖	mathematical	—	DFunLike.coe Module.Dual ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.instFunLike RingHom.id ιMultiDual ιMulti_family Module.Basis Module.Basis.instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	ιMulti_family.eq_1 ιMultiDual_apply_ιMulti Matrix.ext RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_apply RelEmbedding.instEmbeddingLike Matrix.det.congr_simp Matrix.det_one
ιMultiDual_apply_nondiag 📖	mathematical	—	DFunLike.coe Module.Dual ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.instFunLike RingHom.id ιMultiDual ιMulti_family Module.Basis Module.Basis.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	ιMulti_family.eq_1 ιMultiDual_apply_ιMulti Set.powersetCard.exists_mem_notMem_iff_ne Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem Matrix.det_eq_zero_of_column_eq_zero RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_eq_of_ne Subtype.prop Set.powersetCard.ofFinEmbEquiv_symm_apply Set.powersetCard.mem_coe_iff Finset.orderEmbOfFin_mem
ιMultiDual_apply_ιMulti 📖	mathematical	—	DFunLike.coe Module.Dual ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.instFunLike RingHom.id ιMultiDual AlternatingMap AlternatingMap.instFunLike ιMulti Matrix.det Fin.fintype Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of LinearMap Module.Basis.coord OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderEmbedding Set.Elem Finset Set.powersetCard Equiv.symm Set.powersetCard.ofFinEmbEquiv	—	RingHomInvPair.ids pairingDual_ιMulti_ιMulti
ιMulti_family_linearIndependent_field 📖	mathematical	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Set.Elem Finset Set.powersetCard ExteriorAlgebra EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower ιMulti_family Submodule.addCommMonoid Submodule.module	—	Submodule.coe_subtype Module.Basis.span_apply map_comp_ιMulti_family LinearIndependent.map' Module.Basis.linearIndependent coe_basis LinearMap.ker_eq_bot map_injective_field Submodule.subtype_injective
ιMulti_family_linearIndependent_ofBasis 📖	mathematical	—	LinearIndependent Set.Elem Finset Set.powersetCard ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower ιMulti_family DFunLike.coe Module.Basis Module.Basis.instFunLike Submodule.addCommMonoid Submodule.module	—	LinearIndependent.of_pairwise_dual_eq_zero_one ιMultiDual_apply_nondiag ιMultiDual_apply_diag

---

← Back to Index