mul_inv_cancel — Mathlib

English

For nonzero x, x * x⁻¹ = 1 in CauSeq.Completion.Cauchy abv.

Русский

Для ненулевого x: x · x⁻¹ = 1 в CauSeq.Completion.Cauchy abv.

LaTeX

$$x ≠ 0 → x * x⁻¹ = 1$$

Lean4

protected theorem mul_inv_cancel {x : (Cauchy abv)} : x ≠ 0 → x * x⁻¹ = 1 :=
  Quotient.inductionOn x fun f hf => by
    simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
    simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]
    exact Quotient.sound (CauSeq.mul_inv_cancel hf)

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