Documentation Verification Report

Bilinear

📁 Source: Mathlib/Algebra/Algebra/Bilinear.lean

Statistics

Metric	Count
Definitions `lmul`, `mul`, `mul'`, `mul''`, `lmul`, `termμ`, `«termμ[_]»`	7
Theorems `comp_mul'`, `coe_lmul_eq_mul`, `lmul_injective`, `lmul_isUnit_iff`, `commute_mulLeft_right`, `flip_mul`, `lift_lsmul_mul_eq_lsmul_lift_lsmul`, `map_mul_iff`, `mul''_apply`, `mul'_apply`, `mul'_comm`, `mul'_comp_comm`, `mul_apply'`, `mul_apply_apply`, `pow_mulLeft`, `pow_mulRight`, `toSpanSingleton_eq_algebra_linearMap`, `toSpanSingleton_one_eq_algebraLinearMap`, `coe_lmul_eq_mul`, `comp_mul'`	20
Total	27

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_mul'` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `toLinearMap` `LinearMap.mul'` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.map`	—	`TensorProduct.ext'` `RingHomCompTriple.ids` `Algebra.to_smulCommClass` `IsScalarTower.right` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `instNonUnitalAlgHomClassOfAlgHomClass` `algHomClass`

Algebra

Definitions

Name	Category	Theorems
`lmul` 📖	CompOp	11 math math: `lmul_algebraMap`, `lmul_injective`, `toMatrix_lmul'`, `Ideal.constr_basisSpanSingleton`, `isNilpotent_tensor_residueField_iff`, `norm_apply`, `baseChange_lmul`, `lmul_isUnit_iff`, `coe_lmul_eq_mul`, `trace_apply`, `leftMulMatrix_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lmul_eq_mul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Module.End` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `Module.End.instSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lmul` `LinearMap` `RingHom.id` `LinearMap.addCommMonoid` `LinearMap.module` `LinearMap.instFunLike` `LinearMap.mul` `to_smulCommClass` `IsScalarTower.right`	—	`smulCommClass_self` `IsScalarTower.left`
`lmul_injective` 📖	mathematical	—	`Module.End` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `DFunLike.coe` `AlgHom` `Module.End.instSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lmul`	—	`smulCommClass_self` `IsScalarTower.left` `mul_one` `DFunLike.congr_fun`
`lmul_isUnit_iff` 📖	mathematical	—	`IsUnit` `Module.End` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `Module.End.instMonoid` `DFunLike.coe` `AlgHom` `Module.End.instSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lmul`	—	`smulCommClass_self` `IsScalarTower.left` `Module.End.isUnit_iff` `IsUnit.isUnit_iff_mulLeft_bijective`

LinearMap

Definitions

Name	Category	Theorems
`mul` 📖	CompOp	20 math math: `mul_apply_apply`, `NonUnitalAlgHom.coe_lmul_eq_mul`, `Ideal.range_mul'`, `mul_apply'`, `Ideal.range_mul`, `Algebra.IsEpi.injective_lift_mul`, `flip_mul`, `map_mul_iff`, `mul''_apply`, `lift_lsmul_mul_eq_lsmul_lift_lsmul`, `CliffordAlgebra.forall_mul_self_eq_iff`, `QuadraticMap.associated_linMulLin`, `Ideal.subtype_isoBaseOfIsPrincipal_eq_mul`, `Algebra.norm_eq_zero_iff'`, `Submodule.mul_eq_map₂`, `QuadraticMap.associated_sq`, `Algebra.coe_lmul_eq_mul`, `Bialgebra.mul_compr₂_comul`, `Bialgebra.mul_compr₂_counit`, `mulLinearMap_eq_mul`
`mul'` 📖	CompOp	21 math math: `Pi.comul_eq_adjoint`, `convMul_def`, `mul'_comp_comm`, `TensorProduct.gradedMul_def`, `AlgHom.comp_mul'`, `intrinsicStar_mul'`, `mul'_apply`, `HopfAlgebra.mul_antipode_rTensor_comul`, `TensorProduct.Algebra.linearMap_comp_mul'`, `HopfAlgebra.mul_antipode_rTensor_comul_apply`, `ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul`, `IsLocalization.bijective_linearMap_mul'`, `Submodule.mulMap_eq_mul'_comp_mapIncl`, `NonUnitalAlgHom.comp_mul'`, `HopfAlgebra.mul_antipode_lTensor_comul_apply`, `mul'_tensor`, `HopfAlgebra.mul_antipode_lTensor_comul`, `Algebra.TensorProduct.lmul'_toLinearMap`, `convMul_apply`, `mul'_comm`, `TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm`
`mul''` 📖	CompOp	1 math math: `mul''_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_mulLeft_right` 📖	mathematical	—	`Commute` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.End.instMul` `mulLeft` `mulRight`	—	`ext` `mul_assoc`
`flip_mul` 📖	mathematical	—	`flip` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `Semiring.toNonAssocSemiring` `mul`	—	`ext` `SMulCommClass.symm` `smulCommClass_self` `mul_comm`
`lift_lsmul_mul_eq_lsmul_lift_lsmul` 📖	mathematical	—	`TensorProduct.lift` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `comp` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `lsmul` `DFunLike.coe` `instFunLike` `mul` `Algebra.to_smulCommClass` `Algebra.id` `IsScalarTower.right` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`TensorProduct.ext'` `smulCommClass_self` `RingHomCompTriple.ids` `Algebra.to_smulCommClass` `IsScalarTower.right` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `semilinearMapClass` `mul_comm`
`map_mul_iff` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `compr₂` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `mul` `compl₂` `RingHomCompTriple.ids` `comp` `addCommMonoid` `module`	—	`smulCommClass_self` `IsScalarTower.left` `RingHomCompTriple.ids` `ext_iff₂`
`mul''_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `instFunLike` `mul''` `AddMonoidHom` `AddZeroClass.toAddZero` `TensorProduct.addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `TensorProduct.liftAux` `CommSemiring.toSemiring` `mul` `IsScalarTower.right`	—	`Algebra.to_smulCommClass`
`mul'_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `mul'` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mul'_comm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `mul'` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `TensorProduct.comm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `mul'_comp_comm`
`mul'_comp_comm` 📖	mathematical	—	`comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `mul'` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `TensorProduct.comm`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `smulCommClass_self` `TensorProduct.lift_comp_comm_eq` `SMulCommClass.symm` `flip_mul`
`mul_apply'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smulCommClass_self`
`mul_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smulCommClass_self`
`pow_mulLeft` 📖	mathematical	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `mulLeft` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_zero` `mulLeft_one` `Module.End.one_eq_id` `pow_succ` `RingHomCompTriple.ids` `mulLeft_mul` `Module.End.mul_eq_comp`
`pow_mulRight` 📖	mathematical	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `mulRight` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_zero` `mulRight_one` `Module.End.one_eq_id` `pow_succ` `pow_succ'` `RingHomCompTriple.ids` `mulRight_mul` `Module.End.mul_eq_comp`
`toSpanSingleton_eq_algebra_linearMap` 📖	mathematical	—	`toSpanSingleton` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Algebra.linearMap`	—	`toSpanSingleton_one_eq_algebraLinearMap`
`toSpanSingleton_one_eq_algebraLinearMap` 📖	mathematical	—	`toSpanSingleton` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Algebra.linearMap`	—	`ext_ring` `one_smul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

NonUnitalAlgHom

Definitions

Name	Category	Theorems
`lmul` 📖	CompOp	1 math math: `coe_lmul_eq_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lmul_eq_mul` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Module.End` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.End.instSemiring` `LinearMap.instDistribMulAction` `RingHom.id` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `instFunLike_1` `lmul` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `LinearMap.instFunLike` `LinearMap.mul`	—	`smulCommClass_self`
`comp_mul'` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.toDistribMulAction` `instFunLike_1` `NonUnitalAlgHomClass.instLinearMapClass` `instNonUnitalAlgSemiHomClass` `LinearMap.mul'` `TensorProduct.map`	—	`TensorProduct.ext'` `RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `instNonUnitalAlgSemiHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass`

RingTheory.LinearMap

Definitions

Name	Category	Theorems
`termμ` 📖	CompOp	—
`«termμ[_]»` 📖	CompOp	—

---

← Back to Index