coe_unitsWithZeroEquiv_eq_units_val

English

The inverse of WithZeroUnitsEquiv is given by symm on the corresponding MulEquiv.

Русский

Обратное отображение WithZeroUnitsEquiv задаётся симметричным отображением MulEquiv.

LaTeX

$$$\\mathrm{MulEquiv.unzero} : (\\mathrm{WithZero}\\alpha \\simeq_* \\mathrm{WithZero}\\beta) \\to (\\alpha \\simeq_* \\beta)$$$

Lean4

theorem coe_unitsWithZeroEquiv_eq_units_val (γ : (WithZero α)ˣ) : ↑(unitsWithZeroEquiv γ) = γ.val := by
  simp only [WithZero.unitsWithZeroEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.coe_unzero]

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