English
In a field, every nonzero element has a unique multiplicative inverse.
Русский
В поле каждый ненулевой элемент имеет единственный обратный по умножению.
LaTeX
$$$\forall x\in R, x\neq 0 \Rightarrow \exists! y\in R\, (x\cdot y = 1)$$$
Lean4
/-- For each field, and for each nonzero element of said field, there is a unique inverse.
Since `IsField` doesn't remember the data of an `inv` function and as such,
a lemma that there is a unique inverse could be useful.
-/
theorem uniq_inv_of_isField (R : Type u) [Ring R] (hf : IsField R) : ∀ x : R, x ≠ 0 → ∃! y : R, x * y = 1 :=
by
intro x hx
apply existsUnique_of_exists_of_unique
· exact hf.mul_inv_cancel hx
· intro y z hxy hxz
calc
y = y * (x * z) := by rw [hxz, mul_one]
_ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
_ = z := by rw [hxy, one_mul]
