mk_le_mk — Mathlib

English

For all a ≠ 1 and b ≠ 1, mk a ha ≤ mk b hb is equivalent to MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b.

Русский

Для любых a ≠ 1 и b ≠ 1 выполняется, что mk a ha ≤ mk b hb тогда и только тогда, когда MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b.

LaTeX

$$$mk\ a\ ha \le mk\ b\ hb \;\iff\; MulArchimedeanClass.mk a \le MulArchimedeanClass.mk b$$$

Lean4

@[to_additive]
theorem mk_le_mk {a : M} (ha : a ≠ 1) {b : M} (hb : b ≠ 1) :
    mk a ha ≤ mk b hb ↔ MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b :=
  .rfl

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