instNatCast — Mathlib

English

There is a canonical embedding of natural numbers into the homogeneous localization, giving (n : HomogeneousLocalization 𝒜 x).val = n.

Русский

Существует каноническое вложение натуральных чисел в однородную локализацию, при котором (n : HomogeneousLocalization 𝒜 x).val = n.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; (n : \\mathrm{HomogeneousLocalization}(\\mathcal{A},x)).\\mathrm{val} = n$$$

Lean4

instance : NatCast (HomogeneousLocalization 𝒜 x) :=
  ⟨Nat.unaryCast⟩

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