mem_toCotangent_ker

Mathlib.RingTheory.Ideal.Cotangent

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

English

For x ∈ I, x ∈ LinearMap.ker I.toCotangent iff x ∈ I^2.

Русский

Для x ∈ I верно: x ∈ ker(I.toCotangent) ⇔ x ∈ I^2.

LaTeX

$$$x \\in I \\;\\Leftrightarrow\\; x \\in I^2$ в условиях соответствующих отображений$$

Lean4

theorem mem_toCotangent_ker {x : I} : x ∈ LinearMap.ker I.toCotangent ↔ (x : R) ∈ I ^ 2 :=
  by
  rw [← I.map_toCotangent_ker]
  simp

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

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

Разделы

Аффилиация

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