Pairing

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

Statistics

Metric	Count
Definitions alternatingMapToDual, pairingDual, toTensorPower	3
Theorems alternatingMapToDual_apply_ιMulti, pairingDual_apply_apply_eq_one, pairingDual_apply_apply_eq_one_zero, pairingDual_ιMulti_ιMulti, toTensorPower_apply_ιMulti	5
Total	8

exteriorPower

Definitions

Name	Category	Theorems
alternatingMapToDual 📖	CompOp	1 math math: alternatingMapToDual_apply_ιMulti
pairingDual 📖	CompOp	3 math math: pairingDual_ιMulti_ιMulti, pairingDual_apply_apply_eq_one, pairingDual_apply_apply_eq_one_zero
toTensorPower 📖	CompOp	1 math math: toTensorPower_apply_ιMulti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatingMapToDual_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 AlternatingMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id AlternatingMap.instFunLike alternatingMapToDual ιMulti Matrix.det Fin.fintype Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of	—	Algebra.to_smulCommClass toTensorPower_apply_ιMulti map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr map_zsmul_unit TensorPower.multilinearMapToDual_apply_tprod Matrix.det_apply Finset.prod_congr
pairingDual_apply_apply_eq_one 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ExteriorAlgebra Submodule NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap LinearMap.addCommGroup Ring.toAddCommGroup LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.addCommMonoid pairingDual AlternatingMap AlternatingMap.instFunLike ιMulti OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderEmbedding	—	Algebra.to_smulCommClass pairingDual_ιMulti_ιMulti Matrix.det_one Matrix.ext Matrix.one_apply_eq RelEmbedding.instEmbeddingLike Matrix.one_apply_ne
pairingDual_apply_apply_eq_one_zero 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ExteriorAlgebra Submodule NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.addCommMonoid pairingDual AlternatingMap AlternatingMap.instFunLike ιMulti OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderEmbedding	—	Algebra.to_smulCommClass pairingDual_ιMulti_ιMulti Matrix.det_apply Finset.sum_eq_zero Finset.prod_congr smul_zero Finset.prod_eq_zero RelEmbedding.map_rel_iff Equiv.surjective Equiv.symm_apply_apply Equiv.injective le_antisymm LT.lt.le RelEmbedding.ext Equiv.Perm.ext DFunLike.congr_fun OrderIso.subsingleton_of_wellFoundedGT' IsWellOrder.toIsWellFounded isWellOrder_gt Finite.to_wellFoundedGT Finite.of_fintype
pairingDual_ιMulti_ι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 LinearMap LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.addCommMonoid pairingDual AlternatingMap AlternatingMap.instFunLike ιMulti Matrix.det Fin.fintype Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of	—	Algebra.to_smulCommClass alternatingMapLinearEquiv_apply_ιMulti alternatingMapToDual_apply_ιMulti
toTensorPower_apply_ιMulti 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring 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 TensorPower Submodule.addCommMonoid PiTensorProduct.instAddCommMonoid Submodule.module PiTensorProduct.instModule LinearMap.instFunLike toTensorPower AlternatingMap AlternatingMap.instFunLike ιMulti Finset.sum Equiv.Perm PiTensorProduct Finset.univ Equiv.instFintype Fin.fintype Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PiTensorProduct.instAddCommGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign MultilinearMap MultilinearMap.instFunLikeForall PiTensorProduct.tprod EquivLike.toFunLike Equiv.instEquivLike	—	RingHomInvPair.ids smulCommClass_self alternatingMapLinearEquiv_apply_ιMulti MultilinearMap.alternatization_apply Finset.sum_congr

---

← Back to Index