toCotangent_eq

Mathlib.RingTheory.Ideal.Cotangent

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

English

Equality I.toCotangent x = I.toCotangent y holds if and only if (x - y) ∈ I^2.

Русский

Равенство I.toCotangent x = I.toCotangent y эквивалентно (x - y) ∈ I^2.

LaTeX

$$$I.toCotangent x = I.toCotangent y \\iff (x - y) \\in I^2$$$

Lean4

theorem toCotangent_eq {x y : I} : I.toCotangent x = I.toCotangent y ↔ (x - y : R) ∈ I ^ 2 :=
  by
  rw [← sub_eq_zero]
  exact I.mem_toCotangent_ker

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

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

Разделы

Аффилиация

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