mk

Mathlib.RingTheory.Extension.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.Extension.Cotangent.mk

← MathLib Explorer

English

Cotangent.mk x = 0 iff x lies in the square of the kernel.

Русский

Cotangent.mk x = 0 тогда и только тогда, когда x ∈ ker^2.

LaTeX

$$$$ Cotangent.mk x = 0 \iff x ∈ P.ker^2 $$$$

Lean4

/-- The quotient map from the kernel of `P → S` onto the cotangent space. -/
noncomputable def mk : P.ker →ₗ[P.Ring] P.Cotangent
    where
  toFun x := .of (Ideal.toCotangent _ x)
  map_add' x y := by simp
  map_smul' x y := ext <| by simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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