English
The induced map on abelianizations respects composition: the abelianization of the transitive composition equals the composition of abelianizations.
Русский
Индуцированное отображение на абелизациях сохраняет композицию: абелизация композиции равна композиции абелизаций.
LaTeX
$$$ (e^{ab})\circ (e'^{ab}) = (e\circ e')^{ab} $, where e: G ≅ H and e': H ≅ I.$$
Lean4
/-- The subgroup generated by an element of a group equals the set of
integer powers of the element, such that each power is a unique element.
This is the stronger version of `Subgroup.mem_closure_singleton`. -/
@[to_additive /-- The additive subgroup generated by an element of an additive group equals the set
of integer multiples of the element, such that each multiple is a unique element.
This is the stronger version of `AddSubgroup.mem_closure_singleton`. -/
]
theorem mem_closure_singleton_iff_existsUnique_zpow {G : Type*} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G]
{a b : G} (ha : a ≠ 1) : b ∈ closure { a } ↔ ∃! k : ℤ, a ^ k = b :=
by
rw [mem_closure_singleton]
constructor
· suffices Function.Injective (a ^ · : ℤ → G) by
rintro ⟨m, rfl⟩
exact ⟨m, rfl, fun k hk ↦ this hk⟩
rcases ha.lt_or_gt with ha | ha
· exact (zpow_right_strictAnti ha).injective
· exact (zpow_right_strictMono ha).injective
· exact fun h ↦ h.exists
