End

📁 Source: Mathlib/Algebra/Group/Hom/End.lean

Statistics

Metric	Count
Definitions instAddMonoidWithOne, instRing, instSemiring	3
Theorems natCast_apply, ofNat_apply	2
Total	5

AddMonoid.End

Definitions

Name	Category	Theorems
instAddMonoidWithOne 📖	CompOp	11 math math: natCast_apply, two_nsmul_lie_lmul_lmul_add_add_eq_zero, CentroidHom.toEnd_smul, smul_apply, isCentralScalar, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, natCast_def, CentroidHom.toEnd_natCast, smulCommClass, isScalarTower, coe_smul
instRing 📖	CompOp	8 math math: CentroidHom.toEnd_sub, WithLp.idemSnd_compl, two_nsmul_lie_lmul_lmul_add_add_eq_zero, WithLp.idemFst_compl, addMonoidEndRingEquivInt_apply, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, WithLp.idemFst_add_idemSnd, addMonoidEndRingEquivInt_symm_apply
instSemiring 📖	CompOp	7 math math: AddMonoidAlgebra.divOfHom_apply_apply, CentroidHom.centroid_eq_centralizer_mulLeftRight, CentroidHom.toEnd_add, CentroidHom.toEnd_zero, CentroidHom.toEndRingHom_apply, NonUnitalNonAssocSemiring.mem_center_iff, Module.toAddMonoidEnd_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_apply 📖	mathematical	—	DFunLike.coe AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike AddMonoidWithOne.toNatCast instAddMonoidWithOne AddMonoid.toNatSMul	—	—
ofNat_apply 📖	mathematical	—	DFunLike.coe AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike AddMonoid.toNatSMul	—	—

---

← Back to Index