coe_ideal_span_singleton_div_self

English

The product of spanSingleton x with its inverse equals 1 when x ≠ 0.

Русский

Произведение spanSingleton 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_div_self {x : R₁} (hx : x ≠ 0) :
    (Ideal.span ({ x } : Set R₁) : FractionalIdeal R₁⁰ K) / Ideal.span ({ x } : Set R₁) = 1 := by
  rw [coeIdeal_span_singleton,
    spanSingleton_div_self K <| (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx]

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