Dual

📁 Source: Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean

Statistics

Metric	Count
Definitions dualDistrib, dualDistribEquiv, dualDistribEquivOfBasis, dualDistribInvOfBasis	4
Theorems dualDistribEquivOfBasis_apply_apply, dualDistribEquivOfBasis_symm_apply, dualDistribInvOfBasis_apply, dualDistrib_apply, dualDistrib_dualDistribInvOfBasis_left_inverse, dualDistrib_dualDistribInvOfBasis_right_inverse	6
Total	10

PiTensorProduct

Definitions

Name	Category	Theorems
dualDistrib 📖	CompOp	3 math math: dualDistrib_apply, dualDistrib_dualDistribInvOfBasis_right_inverse, dualDistrib_dualDistribInvOfBasis_left_inverse
dualDistribEquiv 📖	CompOp	—
dualDistribEquivOfBasis 📖	CompOp	2 math math: dualDistribEquivOfBasis_symm_apply, dualDistribEquivOfBasis_apply_apply
dualDistribInvOfBasis 📖	CompOp	4 math math: dualDistribEquivOfBasis_symm_apply, dualDistribInvOfBasis_apply, dualDistrib_dualDistribInvOfBasis_right_inverse, dualDistrib_dualDistribInvOfBasis_left_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualDistribEquivOfBasis_apply_apply 📖	mathematical	Finite	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct AddCommGroup.toAddCommMonoid instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike dualDistribEquivOfBasis AlgEquiv instSemiring instAlgebra AlgEquiv.instFunLike constantBaseRingEquiv Fintype.ofFinite Algebra.toModule piTensorHomMap	—	RingHomInvPair.ids Algebra.to_smulCommClass
dualDistribEquivOfBasis_symm_apply 📖	mathematical	Finite	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Dual PiTensorProduct AddCommGroup.toAddCommMonoid instAddCommMonoid instModule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id NonAssocSemiring.toNonUnitalNonAssocSemiring EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm dualDistribEquivOfBasis LinearMap LinearMap.instFunLike dualDistribInvOfBasis	—	RingHomInvPair.ids Algebra.to_smulCommClass
dualDistribInvOfBasis_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual PiTensorProduct AddCommGroup.toAddCommMonoid instAddCommMonoid instModule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike dualDistribInvOfBasis Finite.of_fintype Finset.sum Finset.univ Pi.instFintype instSMul MultilinearMap MultilinearMap.instFunLikeForall tprod Module.Basis Module.Basis.instFunLike smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Basis.dualBasis	—	Algebra.to_smulCommClass Finite.of_fintype smulCommClass_self Finset.sum_congr RingHomInvPair.ids LinearMap.comp.congr_simp Module.Basis.coe_dualBasis LinearMap.coe_sum Finset.sum_apply Lean.Meta.FastSubsingleton.elim Fintype.instFastSubsingleton
dualDistrib_apply 📖	mathematical	—	DFunLike.coe Module.Dual PiTensorProduct CommSemiring.toSemiring instAddCommMonoid instModule LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id dualDistrib Finite.of_fintype MultilinearMap MultilinearMap.instFunLikeForall tprod Finset.prod CommSemiring.toCommMonoid Finset.univ	—	Algebra.to_smulCommClass Finite.of_fintype dualDistrib.eq_1 Fintype.subsingleton piTensorHomMap_tprod_tprod constantBaseRingEquiv_tprod
dualDistrib_dualDistribInvOfBasis_left_inverse 📖	mathematical	Finite	LinearMap.comp Module.Dual PiTensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring instAddCommMonoid instModule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id RingHomCompTriple.ids dualDistrib dualDistribInvOfBasis LinearMap.id	—	Module.Basis.ext smulCommClass_self Pi.finite Algebra.to_smulCommClass RingHomCompTriple.ids Module.Basis.coe_dualBasis Finite.of_fintype dualDistribInvOfBasis_apply Finset.sum_congr RingHomInvPair.ids Basis.piTensorProduct_repr_tprod_apply Finset.prod_congr Module.Basis.repr_self Finsupp.single_apply Fintype.prod_ite_zero Finset.prod_const_one ite_smul one_smul zero_smul Finset.sum_ite_eq' Basis.piTensorProduct_apply dualDistrib_apply
dualDistrib_dualDistribInvOfBasis_right_inverse 📖	mathematical	Finite	LinearMap.comp PiTensorProduct CommRing.toCommSemiring Module.Dual CommSemiring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id instAddCommMonoid instModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHomCompTriple.ids dualDistribInvOfBasis dualDistrib LinearMap.id	—	Module.Basis.ext Algebra.to_smulCommClass RingHomCompTriple.ids Module.Basis.ext_elem RingHomInvPair.ids Basis.piTensorProduct_apply smulCommClass_self Module.Basis.coe_dualBasis Finite.of_fintype dualDistribInvOfBasis_apply Finset.sum_congr dualDistrib_apply Finset.prod_congr Module.Basis.repr_self Finsupp.single_apply Fintype.prod_ite_zero Finset.prod_const_one ite_smul one_smul zero_smul Finset.sum_ite_eq' Basis.piTensorProduct_repr_tprod_apply Module.Basis.dualBasis_repr

---

← Back to Index