toCotangent_eq_zero

Mathlib.RingTheory.Ideal.Cotangent

URI: https://scilib.ai/kg/mathlib#Ideal.toCotangent_eq_zero

English

For x ∈ I, I.toCotangent x = 0 if and only if x ∈ I^2.

Русский

Для x ∈ I, I.toCotangent x = 0 тогда и только тогда, когда x ∈ I^2.

LaTeX

$$$I.toCotangent x = 0 \\iff x \\in I^2$$$

Lean4

theorem toCotangent_eq_zero (x : I) : I.toCotangent x = 0 ↔ (x : R) ∈ I ^ 2 :=
  I.mem_toCotangent_ker

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

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

Разделы

Аффилиация

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