mul_inv_cancel — Mathlib

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

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