English
Let α be a division semiring of characteristic zero. The natural embedding of the nonnegative rationals into α preserves addition: for all p, q ∈ ℚ≥0, the image of p+q in α equals the sum of the images of p and q.
Русский
Пусть α — единично делимый полугруппной кольцо нулевой характеристики. Естественное вложение неотрицательных рациональных чисел в α сохраняет сложение: для любых p, q ∈ ℚ≥0 образ p+q в α равен сумме образов p и q.
LaTeX
$$$ (p+q : \alpha) = (p : \alpha) + (q : \alpha) $$$
Lean4
@[simp, norm_cast]
theorem cast_add (p q : ℚ≥0) : ↑(p + q) = (p + q : α) :=
cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')
