mem_conductor_iff

Mathlib.RingTheory.Conductor

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

English

The mem_conductor_iff statement: y ∈ conductor(R,x) if and only if ∀ z ∈ S, y z ∈ R<x>.

Русский

Пусть y ∈ S принадлежит conductor(R,x) тогда и только тогда, когда ∀ z ∈ S, y z ∈ R<x>.

LaTeX

$$$y \\in \\mathrm{conductor}(R,x) \\iff \\forall z \\in S,\; y z \\in R\\langle x\\rangle$$$

Lean4

theorem mem_conductor_iff {y : S} : y ∈ conductor R x ↔ ∀ b : S, y * b ∈ R<x> :=
  ⟨fun h => h, fun h => h⟩

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

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

Разделы

Аффилиация

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