instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal

English

There is a natural embedding of natural numbers into SlashInvariantForm(Γ,0) sending n to the constant function n.

Русский

Существуют вложения натуральных чисел в SlashInvariantForm(Γ,0), отображающие n в константную функцию n.

LaTeX

$$$n \mapsto (n : \mathrm{SlashInvariantForm}(\Gamma,0))\quad\text{передаёт } n\text{ как константную функцию } n.$$$

Lean4

instance [Γ.HasDetPlusMinusOne] : NatCast (SlashInvariantForm Γ 0) where natCast n := constℝ n

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