one_smul_sub_smul_one_mem_ideal

Mathlib.RingTheory.Kaehler.Basic

URI: https://scilib.ai/kg/mathlib#KaehlerDifferential.one_smul_sub_smul_one_mem_ideal

English

For Kaehler differentials, the element 1 ⊗ s − s ⊗ 1 lies in the Kaehler differential ideal.

Русский

Элемент 1 ⊗ s − s ⊗ 1 принадлежит идеалу KaehlerDifferential.

LaTeX

$$(1 \otimes s) - (s \otimes 1) \in \operatorname{KaehlerDifferential.ideal}(R,S)$$

Lean4

theorem one_smul_sub_smul_one_mem_ideal (a : S) : (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ KaehlerDifferential.ideal R S :=
  by simp [RingHom.mem_ker]

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

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

Разделы

Аффилиация

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