coe_ideal_span_singleton_mul_inv — Mathlib

English

The product of the principal ideal span{x} with its inverse equals 1 for x ≠ 0.

Русский

Произведение главного идеала span{x} на его обратное равно 1 для x ≠ 0.

LaTeX

$$$$ (\mathrm{Ideal.span}\{x\}) (\mathrm{FractionalIdeal}(\mathrm{nonZeroDivisors})\, x)^{-1} = 1,\quad x \neq 0.$$$$

Lean4

theorem coe_ideal_span_singleton_mul_inv {x : R₁} (hx : x ≠ 0) :
    (Ideal.span ({ x } : Set R₁) : FractionalIdeal R₁⁰ K) * (Ideal.span ({ x } : Set R₁) : FractionalIdeal R₁⁰ K)⁻¹ =
      1 :=
  by
  rw [coeIdeal_span_singleton,
    spanSingleton_mul_inv K <| (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx]

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