instCharZero — Mathlib

English

The nonnegative rationals form a characteristic-zero algebraic structure; in particular, the coercion to ℚ is injective.

Русский

У множества неотрицательных рациональных чисел характеристика ноль; в частности, неотрицательный перевод в ℚ инъективен.

LaTeX

$$CharZero \mathbb{Q}_{\ge 0}$$

Lean4

instance instCharZero : CharZero ℚ≥0 where cast_injective a b hab := by simpa using congr_arg num hab

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