Embedding

📁 Source: Mathlib/Algebra/AffineMonoid/Embedding.lean

Statistics

Metric	Count
Definitions dim, embedding	2
Theorems embedding_injective	1
Total	3

AffineAddMonoid

Definitions

Name	Category	Theorems
dim 📖	CompOp	1 math math: embedding_injective
embedding 📖	CompOp	1 math math: embedding_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embedding_injective 📖	mathematical	—	FreeAbelianGroup dim DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup FreeAbelianGroup.addCommGroup AddMonoidHom.instFunLike embedding	—	RingHomInvPair.ids EquivLike.toEmbeddingLike AddLocalization.mk_left_injective AddCancelMonoid.toIsCancelAdd

---

← Back to Index