English
Any nonzero p in RatFunc(K) has a two-sided inverse: p ≠ 0 ⇒ p * p⁻¹ = 1.
Русский
Любой ненулевой элемент RatFunc(K) имеет обратный: p ≠ 0 ⇒ p · p^{-1} = 1.
LaTeX
$$$\forall p\in \mathrm{RatFunc}(K),\; p \neq 0 \Rightarrow p \cdot p^{-1} = 1$$$
Lean4
theorem mul_inv_cancel : ∀ {p : RatFunc K}, p ≠ 0 → p * p⁻¹ = 1
| ⟨p⟩, h => by
have : p ≠ 0 := fun hp => h <| by rw [hp, ofFractionRing_zero]
simpa only [← ofFractionRing_inv, ← ofFractionRing_mul, ← ofFractionRing_one, ofFractionRing.injEq] using
mul_inv_cancel₀ this