spanSingleton_inv_mul — Mathlib

English

The inverse of spanSingleton x multiplied by spanSingleton x equals 1 for x ≠ 0.

Русский

Обратное к spanSingleton x умноженное на spanSingleton x равно 1 при x ≠ 0.

LaTeX

$$$$ (\mathrm{spanSingleton}(x))^{-1} \cdot \mathrm{spanSingleton}(x) = 1,\quad x \neq 0.$$$$

Lean4

theorem spanSingleton_inv_mul {x : K} (hx : x ≠ 0) : (spanSingleton R₁⁰ x)⁻¹ * spanSingleton R₁⁰ x = 1 := by
  rw [mul_comm, spanSingleton_mul_inv K hx]

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