eq_mk'_iff_mul_eq — Mathlib

English

Let f be a localization map from a submonoid S of a commutative monoid M to a commutative monoid N. For elements x ∈ M, y ∈ S, and z ∈ N, the equality z = f.mk' x y holds if and only if z · f(y) = f(x).

Русский

Пусть f — отображение локализации подмножества S ⊆ M в коммутативный моноид N. Для элементов x ∈ M, y ∈ S и z ∈ N справедливо z = f.mk' x y тогда и только тогда z · f(y) = f(x).

LaTeX

$$$ z = f.mk' x y \\iff z \\cdot f y = f x $$$

Lean4

@[to_additive]
theorem eq_mk'_iff_mul_eq {x} {y : S} {z} : z = f.mk' x y ↔ z * f y = f x :=
  ⟨fun H ↦ by rw [H, mk'_spec], fun H ↦ by rwa [mk', mul_inv_right]⟩

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