mulArchimedean_iff — Mathlib

English

A group with zero built from an additive group preserves the Archimedean property across the zero-extended construction.

Русский

Группа с нулем, построенная из аддитивной группы, сохраняет архимедово свойство в нулевой расширенной конструкции.

LaTeX

$$$\mathrm{MulArchimedean}(\mathrm{WithZero}(\,\cdot\,)) \iff \mathrm{MulArchimedean}(\cdot)$$$

Lean4

theorem mulArchimedean_iff {α} [CommGroup α] [PartialOrder α] : MulArchimedean (WithZero α) ↔ MulArchimedean α :=
  by
  constructor <;> intro _
  · exact OrderMonoidIso.unitsWithZero.mulArchimedean
  · infer_instance

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