eq_zero_iff_mem

Mathlib.RingTheory.Ideal.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.eq_zero_iff_mem

English

mk I a = 0 if and only if a ∈ I.

Русский

mk I a = 0 если и только если a ∈ I.

LaTeX

$$$\\pi_I(a) = 0 \\iff a \\in I$$$

Lean4

theorem eq_zero_iff_mem : mk I a = 0 ↔ a ∈ I :=
  Submodule.Quotient.mk_eq_zero _

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

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

Разделы

Аффилиация

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