Bilinear

📁 Source: Mathlib/LinearAlgebra/Quotient/Bilinear.lean

Statistics

Metric	Count
Definitions liftQ₂, liftQ₂	2
Theorems liftQ₂_mk	1
Total	3

LinearMap

Definitions

Name	Category	Theorems
liftQ₂ 📖	CompOp	1 math math: liftQ₂_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftQ₂_mk 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ker LinearMap addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction flip	DFunLike.coe LinearMap Ring.toSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module instFunLike addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction liftQ₂	—	SMulCommClass.symm

LinearMap.IsRefl

Definitions

Name	Category	Theorems
liftQ₂ 📖	CompOp	—

---

← Back to Index