eq' — Mathlib

English

For a localization map f, equality f.mk' a1 a2 = f.mk' b1 b2 is equivalent to the existence of an element of S whose multiplication equates the cross terms via f.mk'.

Русский

Для отображения локализации f равенство f.mk' a1 a2 = f.mk' b1 b2 эквивалентно существованию элемента S, чье умножение приводит к равенству поперечных членов через f.mk'.

LaTeX

$$$ f.mk' a_1 a_2 = f.mk' b_1 b_2 \iff \exists c : S, \; c \cdot (b_2 \cdot a_1) = c \cdot (a_2 \cdot b_1) $$$

Lean4

@[to_additive]
protected theorem eq' {a₁ b₁} {a₂ b₂ : S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ Localization.r S (a₁, a₂) (b₁, b₂) := by
  rw [f.eq, Localization.r_iff_exists]

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