mul_def — Mathlib

English

The set of additive automorphisms of an additive group A forms a group under composition, with the group operation defined by g * h = g ∘ h, identity as Refl, and inverse as Symm.

Русский

Множество аддитивных автоморфизмов группы A образует группу под конкатенацией: произведение задаётся как композиция, единица — тождественный отображение, обратное — обратное.

LaTeX

$$$\text{Group} (AddAut\ A),\; \text{mul } g\; h = g \circ h,\; \text{one } = \mathrm{Refl},\; \text{inv } = \mathrm{Symm}$$$

Lean4

theorem mul_def (e₁ e₂ : AddAut A) : e₁ * e₂ = e₂.trans e₁ :=
  rfl

Похожие утверждения