Documentation Verification Report

End

📁 Source: Mathlib/Algebra/Central/End.lean

Statistics

Metric	Count
Definitions	0
Theorems `instEnd`, `conjAlgEquiv_ext_iff`, `conjAlgEquiv_ext_iff'`, `mem_subalgebraCenter_iff`, `mem_subsemiringCenter_iff`	5
Total	5

Algebra.IsCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEnd` 📖	mathematical	—	`Algebra.IsCentral` `Module.End` `Module.End.instSemiring` `Module.End.instAlgebra` `Algebra.toSMul`	—	`Module.End.mem_subalgebraCenter_iff` `center_eq_bot` `LinearMap.ext` `algebraMap_smul`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjAlgEquiv_ext_iff` 📖	mathematical	—	`conjAlgEquiv` `Algebra.toSMul` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.comp_assoc` `Subalgebra.mem_center_iff` `Algebra.IsCentral.center_eq_bot` `Algebra.IsCentral.instEnd` `Algebra.algebraMap_eq_smul_one` `LinearMapClass.map_smul_of_tower` `SemilinearEquivClass.instSemilinearMapClass` `instSemilinearEquivClass` `LinearMap.IsScalarTower.compatibleSMul`
`conjAlgEquiv_ext_iff'` 📖	mathematical	—	`conjAlgEquiv` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toSMul` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instSMulUnitsId`	—	`RingHomInvPair.ids` `ext` `Subsingleton.eq_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `instSemilinearEquivClass` `smul_zero` `conjAlgEquiv_ext_iff` `exists_ne` `one_smul` `smul_smul` `EquivLike.toEmbeddingLike` `mul_comm`

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_subalgebraCenter_iff` 📖	mathematical	—	`Module.End` `Subalgebra` `instSemiring` `instAlgebra` `Algebra.toSMul` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.center` `smulLeft`	—	`mem_center_iff`
`mem_subsemiringCenter_iff` 📖	mathematical	—	`Module.End` `Subsemiring` `Semiring.toNonAssocSemiring` `instSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.center` `smulLeft`	—	`mem_center_iff`

---

← Back to Index