conductor_eq_top_of_powerBasis

Mathlib.RingTheory.Conductor

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

English

For a power basis pb of R ⊆ S, conductor(R, pb.gen) = ⊤.

Русский

Для PB pb.gen, conductor(R, pb.gen) = ⊤.

LaTeX

$$$\\mathrm{conductor}(R, pb\\, .gen) = \\top$$$

Lean4

theorem conductor_eq_top_of_powerBasis (pb : PowerBasis R S) : conductor R pb.gen = ⊤ :=
  conductor_eq_top_of_adjoin_eq_top pb.adjoin_gen_eq_top

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

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

Разделы

Аффилиация

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