archimedeanClassOrderIso_symm_apply

English

The inverse of the archimedean class order iso maps ArchimedeanClass.mk(m) back to ArchimedeanClass.mk(m).

Русский

Обратное отображение archimedeanClassOrderIso отправляет ArchimedeanClass.mk(m) в ArchimedeanClass.mk(m).

LaTeX

$$$(archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (mk m s)) = ArchimedeanClass.mk m$$$

Lean4

@[simp]
theorem archimedeanClassOrderIso_symm_apply (m : M) (s : ℕ+) :
    (archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (mk m s)) = ArchimedeanClass.mk m :=
  rfl

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