withTopOrderIso_symm_apply — Mathlib

English

The symmetric of the withTopOrderIso sends MulArchimedeanClass.mk a to the corresponding finite class mk a ha.

Русский

Симметричное отображение withTopOrderIso отправляет MulArchimedeanClass.mk a в соответствующий конечный класс mk a ha.

LaTeX

$$$(withTopOrderIso M).symm (MulArchimedeanClass.mk a) = mk a h$$$

Lean4

@[to_additive]
theorem withTopOrderIso_symm_apply {a : M} (h : a ≠ 1) : (withTopOrderIso M).symm (MulArchimedeanClass.mk a) = mk a h :=
  WithTop.subtypeOrderIso_symm_apply (MulArchimedeanClass.mk_eq_top_iff.ne.mpr h)

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