mk_eq_mk — Mathlib

English

For any m, m', s, s' in their domain, mk m s = mk m' s' if and only if there exists u in ℕ+ with u • s'.val • m = u • s.val • m'.

Русский

Для любых m, m', s, s' верно: mk m s = mk m' s' эквивалентно существованию u ∈ ℕ+ такого, что u · s'.val · m = u · s.val · m'.

LaTeX

$$$\forall m,m'\in M\, , s,s'\in \mathbb{N}^+,\; mk\,m\,s = mk\,m'\,s' \iff \exists u\in \mathbb{N}^+:\; u \;\text{val} \cdot s'.\text{val} \cdot m = u \cdot s.\text{val} \cdot m'$$$

Lean4

theorem mk_eq_mk {m m' : M} {s s' : ℕ+} : mk m s = mk m' s' ↔ ∃ u : ℕ+, u.val • s'.val • m = u.val • s.val • m' :=
  by
  unfold mk
  rw [LocalizedModule.mk_eq, ↑ⁿ.exists_congr_left]
  rfl

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