natToInt — Mathlib

English

There is a graded order from Nat to α by transporting along the natural embedding into Int, yielding GradeOrder ℤ α from GradeOrder Nat α.

Русский

Существует градационный переход от натурального к целым через естественное включение Nat → Int, образующий GradeOrder ℤ α из GradeOrder Nat α.

LaTeX

$$$[GradeOrder Nat \\alpha] \\Rightarrow [GradeOrder \\mathbb{Z} \\alpha]$$$

Lean4

instance natToInt [GradeOrder ℕ α] : GradeOrder ℤ α :=
  (GradeOrder.liftLeft _ Int.natCast_strictMono) fun _ _ => CovBy.intCast

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