Dual

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

Statistics

Metric	Count
Definitions dotProductEquiv	1
Theorems toMatrix_transpose, toLin_transpose, dotProductEquiv_apply_apply, dotProductEquiv_symm_apply	4
Total	5

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix_transpose 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Module.Dual AddCommGroup.toAddCommMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype Module.Basis.dualBasis instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instFunLike Module.Dual.transpose Matrix.transpose	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype instSMulCommClass toMatrix_apply RingHomCompTriple.ids Module.Basis.dualBasis_repr Module.Basis.dualBasis_apply

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLin_transpose 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype Module.Basis.dualBasis transpose LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike Module.Dual.transpose	—	LinearEquiv.injective smulCommClass_self RingHomInvPair.ids Finite.of_fintype LinearMap.instSMulCommClass LinearMap.toMatrix_toLin LinearMap.toMatrix_transpose

(root)

Definitions

Name	Category	Theorems
dotProductEquiv 📖	CompOp	4 math math: dotProductEquiv_symm_apply, dotProductEquiv_apply_apply, Matrix.toPerfectPairing_apply_apply, Matrix.toPerfectPairing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dotProductEquiv_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike dotProductEquiv dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids Algebra.to_smulCommClass
dotProductEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Dual Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm dotProductEquiv LinearMap.instFunLike LinearMap Pi.module LinearMap.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids Algebra.to_smulCommClass

---

← Back to Index