instDivisionMonoid — Mathlib

English

If G is a group, then Germ l G is a group, with the group operation induced from G.

Русский

Если G — группа, то Germ l G — группа, операция умножения на гермах задаётся по принципу из G.

LaTeX

$$$ \\mathrm{Germ}(l,G) \\text{ is a group}. $$$

Lean4

@[to_additive]
instance instDivisionMonoid [DivisionMonoid G] : DivisionMonoid (Germ l G)
    where
  inv_inv := inv_inv
  mul_inv_rev x y := inductionOn₂ x y fun _ _ ↦ congr_arg ofFun <| mul_inv_rev _ _
  inv_eq_of_mul x
    y := inductionOn₂ x y fun _ _ h ↦ coe_eq.2 <| (coe_eq.1 h).mono fun _ ↦ DivisionMonoid.inv_eq_of_mul _ _

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