eq — Mathlib · SciLib

English

Two formal images f.mk' a1 a2 and f.mk' b1 b2 are equal if and only if there exists some c in S such that c·(b2·a1) = c·(a2·b1).

Русский

Два изображения через фукцию локализации f.mk' a1 a2 и f.mk' b1 b2 равны тогда и только тогда, когда существует c∈S такое, что c·(b2·a1) = c·(a2·b1).

LaTeX

$$$ f.mk' a_1 a_2 = f.mk' b_1 b_2 \iff \exists c \in 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₂ ↔ ∃ c : S, ↑c * (↑b₂ * a₁) = c * (a₂ * b₁) :=
  f.mk'_eq_iff_eq.trans <| f.eq_iff_exists

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