mul_annihilator

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Submodule.mul_annihilator

English

Multiplying an ideal I by its annihilator yields the zero submodule.

Русский

Умножение идеала I на его аннигилятор даёт нулевой подмодуль.

LaTeX

$$$ I \\cdot \\operatorname{annihilator}(I) = \\bot. $$$

Lean4

@[simp]
theorem mul_annihilator (I : Ideal R) : I * annihilator I = ⊥ := by rw [mul_comm, annihilator_mul]

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

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

Разделы

Аффилиация

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