mul_inv_cancel — Mathlib

English

For any nonzero x in K, x multiplied by its inverse equals 1: x * inv(x) = 1.

Русский

Для любого ненулевого элемента x в K выполняется x · inv(x) = 1.

LaTeX

$$∀ x ≠ 0, x \cdot IsFractionRing.inv(A,x) = 1$$

Lean4

protected theorem mul_inv_cancel (x : K) (hx : x ≠ 0) : x * IsFractionRing.inv A x = 1 :=
  by
  rw [IsFractionRing.inv, dif_neg hx, ←
    IsUnit.mul_left_inj
      (map_units K
        ⟨(sec _ x).1,
          mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
            hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
    one_mul, mul_assoc]
  rw [mk'_spec, ← eq_mk'_iff_mul_eq]
  exact (mk'_sec _ x).symm

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