of — Mathlib · SciLib

English

There is a canonical map from the kernel cotangent to the cotangent type, given by identity on elements.

Русский

Существует каноническое отображение ядра котантантного пространства в котантантный тип через тождественный отображение.

LaTeX

$$def of (x : P.ker.Cotangent) : P.Cotangent := x$$

Lean4

/-- The identity map `P.ker.Cotangent → P.Cotangent` into the type synonym. -/
def of (x : P.ker.Cotangent) : P.Cotangent :=
  x

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