instInvOneClass — Mathlib

English

If G has an inverse with unit, then Germ l G also has an inverse with unit; the unit and inverse are transported along the germ construction.

Русский

Если у G есть единица и обратный элемент, то и у Germ l G есть единица и обратный элемент, получаемые по образу их в G.

LaTeX

$$$ \\text{InvOneClass}_{\\mathrm{Germ}}(l,G) \\text{ inherited from } (G,\\mathrm{InvOneClass}) $$$

Lean4

@[to_additive]
instance instInvOneClass [InvOneClass G] : InvOneClass (Germ l G) :=
  ⟨congr_arg ofFun inv_one⟩

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