conductor_subset_adjoin

Mathlib.RingTheory.Conductor

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

English

For any x, conductor(R,x) is contained in the subalgebra R<x>.

Русский

Кондуктор x включён в подалгебру R<x>.

LaTeX

$$$\\mathrm{conductor}(R,x) \\subseteq R\\langle x\\rangle$$$

Lean4

theorem conductor_subset_adjoin : (conductor R x : Set S) ⊆ R<x> := fun y hy => by simpa only [mul_one] using hy 1

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

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

Разделы

Аффилиация

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