coe_ideal_span_singleton_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{FractionalIdeal}.instInvNonZeroDivisors K).inv(\mathrm{FractionalIdeal}.spanSingleton(\mathrm{nonZeroDivisors} R) x) \cdot \mathrm{FractionalIdeal}.spanSingleton(\mathrm{nonZeroDivisors} R) x = 1, \quad x \neq 0.$$$$

Lean4

theorem coe_ideal_span_singleton_inv_mul {x : R₁} (hx : x ≠ 0) :
    (Ideal.span ({ x } : Set R₁) : FractionalIdeal R₁⁰ K)⁻¹ * Ideal.span ({ x } : Set R₁) = 1 := by
  rw [mul_comm, coe_ideal_span_singleton_mul_inv K hx]

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