spanSingleton_div_spanSingleton — Mathlib

English

For x ≠ 0, the division by itself of the principal ideal generated by x equals 1 after localization.

Русский

Для x ≠ 0 деление порожденного идеала по x на сам элемент после локализации равно 1.

LaTeX

$$$$ (\mathrm{Ideal.span}\{x\})^{\uparrow} / \mathrm{Ideal.span}\{x\} = 1,\quad x \neq 0, $$$$

Lean4

theorem spanSingleton_div_spanSingleton (x y : K) :
    spanSingleton R₁⁰ x / spanSingleton R₁⁰ y = spanSingleton R₁⁰ (x / y) := by
  rw [div_spanSingleton, mul_comm, spanSingleton_mul_spanSingleton, div_eq_mul_inv]

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