spanSingleton_mul_inv — Mathlib

English

Let I be a fractional ideal with a principal generator; then I multiplied by the inverse of its generator equals 1 after localization.

Русский

Пусть I — дробный идеал с порождающим один элемент; тогда I умноженное на обратное порождающего элемента даёт 1 после локализации.

LaTeX

$$$$I \cdot \mathrm{spanSingleton}(\text{generator}(I))^{-1} = 1.$$$$

Lean4

theorem spanSingleton_mul_inv {x : K} (hx : x ≠ 0) : spanSingleton R₁⁰ x * (spanSingleton R₁⁰ x)⁻¹ = 1 := by
  rw [spanSingleton_inv, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ hx, spanSingleton_one]

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