mk_lt_mk — Mathlib

English

Let M be a commutative group with a linear order that makes M an ordered monoid. For a, b ∈ M, mk a < mk b if and only if for every natural n, |b|_m^n < |a|_m.

Русский

Пусть M — коммутативная группа с линейным порядком, делающим ее упорядоченным моноидом. Для a, b ∈ M верно: mk a < mk b тогда и только тогда, когда для любого натурального n выполняется |b|_м^n < |a|_м.

LaTeX

$$$mk\ a < mk\ b \iff \forall n \in \mathbb{N},\ |b|_m^n < |a|_m$$$

Lean4

@[to_additive]
theorem mk_lt_mk : mk a < mk b ↔ ∀ n, |b|ₘ ^ n < |a|ₘ :=
  .rfl

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