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 HasQuotient.Quotient Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module instFunLike liftQ₂	—	SMulCommClass.symm

LinearMap.IsRefl

Definitions

Name	Category	Theorems
liftQ₂ 📖	CompOp	—

---

← Back to Index