mk'_eq_iff_eq' — Mathlib

English

Let f be a localization map as above. Then the equality f.mk' x1 y1 = f.mk' x2 y2 holds if and only if f (x1 y2) = f (x2 y1).

Русский

Пусть f — отображение локализации указанного типа. Равенство f.mk' x1 y1 = f.mk' x2 y2 эквивалентно f(x1 y2) = f(x2 y1).

LaTeX

$$$ f.mk' x_1 y_1 = f.mk' x_2 y_2 \iff f(x_1 \cdot y_2) = f(x_2 \cdot y_1) $$$

Lean4

@[to_additive]
theorem mk'_eq_iff_eq' {x₁ x₂} {y₁ y₂ : S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (x₁ * y₂) = f (x₂ * y₁) := by
  simp only [f.mk'_eq_iff_eq, mul_comm]

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