termℙ — Mathlib

English

The projectivization class of a representative equals the original projectivized point.

Русский

Класс проективного пространства представителя равен исходной точке проективного пространства.

LaTeX

$$$ \mathrm{mk}(K, v.rep, v.rep\_nonzero) = v $$$

Lean4

/-- We define notations `ℙ K V` for the projectivization of the `K`-vector space `V`. -/
@[scoped term_parser 1000]
public meta def termℙ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `LinearAlgebra.Projectivization.termℙ 1024 (ParserDescr.symbol✝ "ℙ")

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