conductor_eq_top_iff_adjoin_eq_top

Mathlib.RingTheory.Conductor

URI: https://scilib.ai/kg/mathlib#conductor_eq_top_iff_adjoin_eq_top

← MathLib Explorer

English

The equivalence between conductor being top and adjoin being top.

Русский

Эквивалентность между conductor = ⊤ и adjoin = ⊤.

LaTeX

$$$\\mathrm{conductor}(R,x) = \\top \\iff \\mathrm{adjoin}_R\\{x\\} = \\top$$$

Lean4

theorem conductor_eq_top_iff_adjoin_eq_top {x : S} : conductor R x = ⊤ ↔ Algebra.adjoin R { x } = ⊤ :=
  ⟨fun h ↦ adjoin_eq_top_of_conductor_eq_top h, fun h ↦ conductor_eq_top_of_adjoin_eq_top h⟩

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

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

Разделы

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

Аффилиация

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