mk_eq_mk_iff — Mathlib

English

Two mk's are equal iff they represent the same congruence class under r.

Русский

mk a b = mk c d тогда же, если и только если они представляют один и тот же класс по r.

LaTeX

$$$ mk\ a\ b = mk\ c\ d \iff r\ S\ (a,b) (c,d) $$$

Lean4

@[to_additive]
theorem mk_eq_mk_iff {a c : M} {b d : S} : mk a b = mk c d ↔ r S ⟨a, b⟩ ⟨c, d⟩ := by
  simp only [mk, OreLocalization.oreDiv_eq_iff, r_iff_oreEqv_r, OreLocalization.oreEqv]

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