group — Mathlib

English

The set of affine automorphisms of P1 forms a group under composition, with identity given by the identity affine equivalence, and multiplication given by composition.

Русский

Множество аффинных автоморфизмов P1 образует группу по умнажению через композицию; единица — это тождественное отображение, умножение — композиция.

LaTeX

$$$\operatorname{Aut}_{k}(P_1) \;\text{is a group under composition, with} \; e \cdot e' = e' \circ e, \; e^{-1} = e^{\,-1} = \mathrm{symm}(e)$$$

Lean4

instance group : Group (P₁ ≃ᵃ[k] P₁) where
  one := refl k P₁
  mul e e' := e'.trans e
  inv := symm
  mul_assoc _ _ _ := trans_assoc _ _ _
  one_mul := trans_refl
  mul_one := refl_trans
  inv_mul_cancel := self_trans_symm

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