spanSingleton_inv

Mathlib.RingTheory.FractionalIdeal.Inverse

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.spanSingleton_inv

English

For any x ≠ 0, (spanSingleton x)^{-1} = spanSingleton x^{-1}.

Русский

Для любого x ≠ 0, (spanSingleton x)^{-1} = spanSingleton x^{-1}.

LaTeX

$$$$ (\mathrm{spanSingleton}\,x)^{-1} = \mathrm{spanSingleton}\,x^{-1},\quad x \neq 0.$$$$

Lean4

@[simp]
theorem spanSingleton_inv (x : K) : (spanSingleton R₁⁰ x)⁻¹ = spanSingleton _ x⁻¹ :=
  one_div_spanSingleton x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru