spanSingleton_div_self

Mathlib.RingTheory.FractionalIdeal.Inverse

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

← MathLib Explorer

English

For x ≠ 0, spanSingleton(x) / spanSingleton(x) = 1.

Русский

Для x ≠ 0, spanSingleton(x) / spanSingleton(x) = 1.

LaTeX

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

Lean4

theorem spanSingleton_div_self {x : K} (hx : x ≠ 0) : spanSingleton R₁⁰ x / spanSingleton R₁⁰ x = 1 := by
  rw [spanSingleton_div_spanSingleton, div_self hx, spanSingleton_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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