instGroupWithZero — Mathlib

English

If α is a group, then WithZero α is a group with zero.

Русский

Если α — группа, то WithZero α образует группу с нулём.

LaTeX

$$$\\operatorname{GroupWithZero}(\\mathrm{WithZero}\\ \\alpha)$ \n$$ \\text{(provided } \\operatorname{Group}(\\alpha)\\text{)} $$$$

Lean4

/-- If `α` is a group then `WithZero α` is a group with zero. -/
instance instGroupWithZero : GroupWithZero (WithZero α)
    where
  inv_zero := WithZero.inv_zero
  mul_inv_cancel a
    ha := by
    lift a to α using ha
    norm_cast
    apply mul_inv_cancel

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