English
In the localization S of R at M, the sum of two elements represented by (x1,y1) and (x2,y2) yields the fraction with numerator x1 y2 + x2 y1 and denominator y1 y2; i.e., (x1/y1) + (x2/y2) = (x1 y2 + x2 y1)/(y1 y2).
Русский
В локализации S кольца R по M сумма двух элементов, представленных как дроби x1/y1 и x2/y2, равна (x1 y2 + x2 y1)/(y1 y2).
LaTeX
$$$ \\text{In the localization } \\frac{x_1}{y_1} + \\frac{x_2}{y_2} = \\frac{x_1 y_2 + x_2 y_1}{y_1 y_2}. $$$
Lean4
theorem mk'_add (x₁ x₂ : R) (y₁ y₂ : M) : mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂ :=
mk'_eq_iff_eq_mul.2 <|
Eq.symm
(by
rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul, mul_comm (_ * _), ←
mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul]
simp only [map_add, Submonoid.coe_mul, map_mul]
ring)
