Documentation Verification Report

Bilinear

📁 Source: Mathlib/Data/Matrix/Bilinear.lean

Statistics

Metric	Count
Definitions `mulLeftLinearMap`, `mulLinearMap`, `mulRightLinearMap`	3
Theorems `commute_mulLeftLinearMap_mulRightLinearMap`, `mulLeftLinearMap_apply`, `mulLeftLinearMap_eq_mulLeft`, `mulLeftLinearMap_eq_zero_iff`, `mulLeftLinearMap_mul`, `mulLeftLinearMap_one`, `mulLeftLinearMap_zero_eq_zero`, `mulLinearMap_apply_apply`, `mulLinearMap_eq_mul`, `mulRightLinearMap_apply`, `mulRightLinearMap_eq_mulRight`, `mulRightLinearMap_eq_zero_iff`, `mulRightLinearMap_mul`, `mulRightLinearMap_one`, `mulRightLinearMap_zero_eq_zero`, `pow_mulLeftLinearMap`, `pow_mulRightLinearMap`	17
Total	20

(root)

Definitions

Name	Category	Theorems
`mulLeftLinearMap` 📖	CompOp	8 math math: `commute_mulLeftLinearMap_mulRightLinearMap`, `pow_mulLeftLinearMap`, `mulLeftLinearMap_eq_mulLeft`, `mulLeftLinearMap_one`, `mulLeftLinearMap_zero_eq_zero`, `mulLeftLinearMap_eq_zero_iff`, `mulLeftLinearMap_apply`, `mulLeftLinearMap_mul`
`mulLinearMap` 📖	CompOp	2 math math: `mulLinearMap_apply_apply`, `mulLinearMap_eq_mul`
`mulRightLinearMap` 📖	CompOp	8 math math: `mulRightLinearMap_one`, `mulRightLinearMap_eq_mulRight`, `mulRightLinearMap_zero_eq_zero`, `commute_mulLeftLinearMap_mulRightLinearMap`, `mulRightLinearMap_eq_zero_iff`, `pow_mulRightLinearMap`, `mulRightLinearMap_apply`, `mulRightLinearMap_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_mulLeftLinearMap_mulRightLinearMap` 📖	mathematical	—	`LinearMap.comp` `Matrix` `CommSemiring.toSemiring` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `mulLeftLinearMap` `mulRightLinearMap`	—	`LinearMap.ext` `RingHomCompTriple.ids` `Matrix.mul_assoc`
`mulLeftLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instFunLike` `mulLeftLinearMap` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulLeftLinearMap_eq_mulLeft` 📖	mathematical	—	`mulLeftLinearMap` `LinearMap.mulLeft` `Matrix` `Matrix.nonUnitalNonAssocSemiring` `Matrix.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.Semiring.smulCommClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`mulLeftLinearMap_eq_zero_iff` 📖	mathematical	—	`mulLeftLinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearMap` `RingHom.id` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instZero` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Matrix.ext` `DFunLike.congr_fun` `Matrix.mul_single_apply_same` `mul_one` `Matrix.ext_iff` `mulLeftLinearMap_zero_eq_zero`
`mulLeftLinearMap_mul` 📖	mathematical	—	`mulLeftLinearMap` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `LinearMap.comp` `Matrix.addCommMonoid` `Matrix.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`LinearMap.ext` `RingHomCompTriple.ids` `Matrix.ext` `Matrix.mul_assoc`
`mulLeftLinearMap_one` 📖	mathematical	—	`mulLeftLinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `LinearMap.id` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module`	—	`LinearMap.ext` `Matrix.one_mul`
`mulLeftLinearMap_zero_eq_zero` 📖	mathematical	—	`mulLeftLinearMap` `Matrix` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instZero`	—	`LinearMap.ext` `Matrix.zero_mul`
`mulLinearMap_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `CommMonoid.toMonoid` `mulLinearMap` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Matrix.smulCommClass` `smulCommClass_self`
`mulLinearMap_eq_mul` 📖	mathematical	—	`mulLinearMap` `LinearMap.mul` `Matrix` `Matrix.nonUnitalNonAssocSemiring` `Matrix.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.Semiring.smulCommClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Matrix.Semiring.isScalarTower`	—	`Matrix.smulCommClass` `smulCommClass_self`
`mulRightLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instFunLike` `mulRightLinearMap` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulRightLinearMap_eq_mulRight` 📖	mathematical	—	`mulRightLinearMap` `LinearMap.mulRight` `Matrix` `Matrix.nonUnitalNonAssocSemiring` `Matrix.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.Semiring.isScalarTower` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`mulRightLinearMap_eq_zero_iff` 📖	mathematical	—	`mulRightLinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearMap` `RingHom.id` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instZero` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Matrix.ext` `DFunLike.congr_fun` `Matrix.single_mul_apply_same` `one_mul` `Matrix.ext_iff` `mulRightLinearMap_zero_eq_zero`
`mulRightLinearMap_mul` 📖	mathematical	—	`mulRightLinearMap` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `LinearMap.comp` `Matrix.addCommMonoid` `Matrix.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`LinearMap.ext` `RingHomCompTriple.ids` `Matrix.ext` `Matrix.mul_assoc`
`mulRightLinearMap_one` 📖	mathematical	—	`mulRightLinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `LinearMap.id` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module`	—	`LinearMap.ext` `Matrix.mul_one`
`mulRightLinearMap_zero_eq_zero` 📖	mathematical	—	`mulRightLinearMap` `Matrix` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.module` `LinearMap.instZero`	—	`LinearMap.ext` `Matrix.mul_zero`
`pow_mulLeftLinearMap` 📖	mathematical	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `Monoid.toNatPow` `Module.End.instMonoid` `mulLeftLinearMap` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring`	—	`pow_zero` `mulLeftLinearMap_one` `Module.End.one_eq_id` `pow_succ` `RingHomCompTriple.ids` `mulLeftLinearMap_mul` `Module.End.mul_eq_comp`
`pow_mulRightLinearMap` 📖	mathematical	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `Monoid.toNatPow` `Module.End.instMonoid` `mulRightLinearMap` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring`	—	`pow_zero` `mulRightLinearMap_one` `Module.End.one_eq_id` `pow_succ` `pow_succ'` `RingHomCompTriple.ids` `mulRightLinearMap_mul` `Module.End.mul_eq_comp`

---

← Back to Index