mk_eq_mk_of_mulArchimedean — Mathlib

English

Assume M is MulArchimedean. Then for any a ≠ 1 and b ≠ 1, mk a = mk b.

Русский

Пусть M удовлетворяет условию MulArchimedean. Тогда для любых a ≠ 1 и b ≠ 1 выполняется mk a = mk b.

LaTeX

$$$[\\text{MulArchimedean }M] \\to \\Big( (a \\neq 1) \\to (b \\neq 1) \\to mk(a) = mk(b) \\Big)$$$

Lean4

@[to_additive mk_eq_mk_of_archimedean]
theorem mk_eq_mk_of_mulArchimedean [MulArchimedean M] (ha : a ≠ 1) (hb : b ≠ 1) : mk a = mk b :=
  by
  obtain hm := MulArchimedean.arch |b|ₘ (show 1 < |a|ₘ by simpa using ha)
  obtain hn := MulArchimedean.arch |a|ₘ (show 1 < |b|ₘ by simpa using hb)
  exact mk_eq_mk.mpr ⟨hm, hn⟩

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