mk'_eq_iff_eq_mul — Mathlib

English

For a localization map f, and any x ∈ M, y ∈ S, z ∈ N, the equality f.mk' x y = z is equivalent to f x = z · f y.

Русский

Для отображения локализации f и любых x ∈ M, y ∈ S, z ∈ N равенство f.mk' x y = z эквивалентно f x = z · f y.

LaTeX

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

Lean4

@[to_additive]
theorem mk'_eq_iff_eq_mul {x} {y : S} {z} : f.mk' x y = z ↔ f x = z * f y := by rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]

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