mk_eq — Mathlib

English

Two representatives (m,s) and (m',s') define the same class if and only if there exists u in S with u·s'·m = u·s·m'.

Русский

Две пары дают один и тот же класс тогда и только тогда, когда найдется u в S такое, что u·s'·m = u·s·m'.

LaTeX

$$$\\mk(m,s) = \\mk(m',s') \\iff \\exists u\\in S,\\ u\\,s'\\,m = u\\,s\\,m'.$$$

Lean4

theorem mk_eq {m m' : M} {s s' : S} : mk m s = mk m' s' ↔ ∃ u : S, u • s' • m = u • s • m' :=
  Quotient.eq'

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