withZero — Mathlib

English

There is a canonical correspondence between MulEquiv α β and MulEquiv (WithZero α) (WithZero β).

Русский

Существует каноническое соответствие между MulEquiv α β и MulEquiv (WithZero α) (WithZero β).

LaTeX

$$$\\text{MulEquiv.withZero} : (\\alpha \\simeq_* \\beta) \\to ((WithZero \\alpha) \\simeq_* (WithZero \\beta))$$$

Lean4

/-- A version of `Equiv.optionCongr` for `WithZero`. -/
@[simps!]
def _root_.MulEquiv.withZero [Group β] : (α ≃* β) ≃ (WithZero α ≃* WithZero β)
    where
  toFun
    e :=
    ⟨⟨map' e, map' e.symm, (by induction · <;> simp), (by induction · <;> simp)⟩,
      (by induction · <;> induction · <;> simp)⟩
  invFun
    e :=
    ⟨⟨fun x ↦ unzero (x := e x) (by simp [ne_eq, ← e.eq_symm_apply]), fun x ↦
        unzero (x := e.symm x) (by simp [e.symm_apply_eq]), by intro; simp, by intro; simp⟩,
      by intro; simp [← coe_inj]⟩
  left_inv _ := by ext; simp
  right_inv _ := by ext x; cases x <;> simp

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