English
Let f be a localization map for a submonoid S of a commutative monoid M, with target N. For any x1, x2 in M and y1, y2 in S, the fractions x1/y1 and x2/y2 are identified in the localization exactly when the cross-multiplied images coincide: f(y2·x1) = f(y1·x2).
Русский
Пусть f — отображение локализации для подмоноида S в коммутативном моноиде M, в N. Для любых x1, x2 в M и y1, y2 в S дроби x1/y1 и x2/y2 равны в локализации тогда и только тогда, когда выполняется равенство после перекрестного перемножения: f(y2·x1) = f(y1·x2).
LaTeX
$$$ f\left(\frac{x_1}{y_1}\right) = f\left(\frac{x_2}{y_2}\right) \iff f(y_2 x_1) = f(y_1 x_2) $$$
Lean4
@[to_additive]
theorem mk'_eq_iff_eq {x₁ x₂} {y₁ y₂ : S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (y₂ * x₁) = f (y₁ * x₂)
where
mp H := by rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]
mpr
H := by
rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f y₁), ← mul_assoc, ← map_mul f, mul_comm x₂, ← H, ← mul_comm x₁,
map_mul f, mul_inv_right f.map_units, toMonoidHom_apply]
