conductor_eq_top_of_adjoin_eq_top

Mathlib.RingTheory.Conductor

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

← MathLib Explorer

English

If the conductor equals top, then adjoin of x is top.

Русский

Если conductor(R,x) = top, то Algebra.adjoin(R,{x}) = top.

LaTeX

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

Lean4

theorem conductor_eq_top_of_adjoin_eq_top (h : R<x> = ⊤) : conductor R x = ⊤ := by
  simp only [Ideal.eq_top_iff_one, mem_conductor_iff, h, mem_top, forall_const]

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

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

Разделы

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

Аффилиация

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