AddChar

📁 Source: Mathlib/Algebra/DirectSum/AddChar.lean

Statistics

Metric	Count
Definitions directSum	1
Theorems directSum_apply, directSum_injective	2
Total	3

AddChar

Definitions

Name	Category	Theorems
directSum 📖	CompOp	2 math math: directSum_apply, directSum_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum_apply 📖	mathematical	—	DFunLike.coe AddChar DirectSum AddCommGroup.toAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DirectSum.instAddCommGroup CommMonoid.toMonoid instFunLike directSum AddMonoidHom Additive AddZeroClass.toAddZero AddMonoid.toAddZeroClass Additive.addZeroClass Monoid.toMulOneClass AddMonoidHom.instFunLike DirectSum.toAddMonoid Additive.addCommMonoid Equiv AddCommMonoid.toAddMonoid EquivLike.toFunLike Equiv.instEquivLike toAddMonoidHomEquiv	—	—
directSum_injective 📖	mathematical	—	AddChar DirectSum AddCommGroup.toAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DirectSum.instAddCommGroup CommMonoid.toMonoid directSum	—	Equiv.injective DirectSum.toAddMonoid_injective EquivLike.toEmbeddingLike

---

← Back to Index