English
For any cardinal a, a is a unit in the multiplicative structure if and only if a = 1.
Русский
Для любого кардинала a существование обратного элемента по умножению возможно тогда и только тогда, когда a = 1.
LaTeX
$$$\mathrm{IsUnit}(a) \iff a = 1$$$
Lean4
/-- Alias of `isUnit_iff_eq_one` for discoverability. -/
theorem isUnit_iff : IsUnit a ↔ a = 1 :=
by
refine
⟨fun h => ?_, by
rintro rfl
exact isUnit_one⟩
rcases eq_or_ne a 0 with (rfl | ha)
· exact (not_isUnit_zero h).elim
rw [isUnit_iff_forall_dvd] at h
obtain ⟨t, ht⟩ := h 1
rw [eq_comm, mul_eq_one_iff_of_one_le] at ht
· exact ht.1
· exact one_le_iff_ne_zero.mpr ha
· apply one_le_iff_ne_zero.mpr
intro h
rw [h, mul_zero] at ht
exact zero_ne_one ht
