English
There is a unique unit in ENat; the unit group is a singleton.
Русский
В ENat существует единственный единичный элемент; группа единиц тождественна.
LaTeX
$$$$\text{Unique}(\mathbb{N}_\infty^{\times})$$$$
Lean4
instance : Unique ℕ∞ˣ where
uniq
x := by
have := x.val_inv
have x_top : x.val ≠ ⊤ := by
intro h
simp [h] at this
have x_inv_top : x.inv ≠ ⊤ := by
intro h
simp only [h, ne_eq, x.ne_zero, not_false_eq_true, mul_top, top_ne_one] at this
obtain ⟨y, x_y⟩ := ne_top_iff_exists.1 x_top
obtain ⟨z, x_z⟩ := ne_top_iff_exists.1 x_inv_top
replace x_y := x_y.symm
rw [x_y, ← x_z, ← coe_mul, ← coe_one, coe_inj, _root_.mul_eq_one] at this
rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y
