Matrix

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

Statistics

Metric	Count
Definitions	0
Theorems toPerfectPairing, toPerfectPairing_apply_apply	2
Total	2

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPerfectPairing 📖	mathematical	—	LinearMap.IsPerfPair Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing Pi.Function.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearEquiv.toLinearMap RingHom.id RingHomInvPair.ids Module.Dual Pi.addCommMonoid LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearEquiv.trans RingHomCompTriple.ids toLinearEquiv' dotProductEquiv	—	RingHomInvPair.ids Algebra.to_smulCommClass RingHomCompTriple.ids LinearEquiv.bijective LinearMap.IsPerfPair.bijective_right LinearEquiv.instIsPerfPair Module.instIsReflexiveOfFiniteOfProjective Module.Finite.pi Finite.of_fintype Module.Finite.self Module.Projective.of_free Module.Free.function Module.Free.self
toPerfectPairing_apply_apply 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike RingHom.id LinearEquiv RingHomInvPair.ids NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans RingHomCompTriple.ids toLinearEquiv' dotProductEquiv dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib mulVec	—	RingHomInvPair.ids Algebra.to_smulCommClass RingHomCompTriple.ids

---

← Back to Index