coe_add — Mathlib

English

The coercion from M to DivisibleHull M is compatible with addition: the image of a sum equals the sum of images.

Русский

Коэрцировка из M в DivisibleHull M совместима со сложением: образ суммы равен сумме образов.

LaTeX

$$$\uparrow( m_1 + m_2 ) = \uparrow m_1 + \uparrow m_2$$$

Lean4

@[simp, norm_cast]
theorem coe_add {m1 m2 : M} : ↑(m1 + m2) = (↑m1 + ↑m2 : DivisibleHull M) := by simp [mk_add_mk_left]

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