unitsWithZeroEquiv — Mathlib

English

If α is a group and nontrivial, then the units of WithZero α are nontrivial.

Русский

Если α — группа и не тривиальная, то единицы WithZero α не тривиальны.

LaTeX

$$$\\operatorname{Nontrivial}(\\mathrm{Units}(\\mathrm{WithZero}\\ \\alpha))$$$

Lean4

/-- Any group is isomorphic to the units of itself adjoined with `0`. -/
@[simps]
def unitsWithZeroEquiv : (WithZero α)ˣ ≃* α
    where
  toFun a := unzero a.ne_zero
  invFun a := Units.mk0 a coe_ne_zero
  left_inv _ := Units.ext <| by simp only [coe_unzero, Units.mk0_val]
  map_mul' _ _ := coe_inj.mp <| by simp only [Units.val_mul, coe_unzero, coe_mul]

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