English
The archimedeanClassOrderIso has a symmetric inverse; applying the inverse to an ArchimedeanClass mk yields the corresponding original class.
Русский
У Изоморфизма ArchimedeanClass Order есть обратный, возвращающий исходный класс.
LaTeX
$$archimedeanClassOrderIso_symm_apply (m) (s) : (archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (mk m s)) = ArchimedeanClass.mk m$$
Lean4
/-- `ArchimedeanClass.mk` of an element from `DivisibleHull` only depends on the numerator. -/
theorem archimedeanClassMk_mk_eq (m : M) (s s' : ℕ+) : ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s') :=
by
suffices (s : ℤ) • mk m s = (s' : ℤ) • mk m s'
by
apply_fun ArchimedeanClass.mk at this
rw [ArchimedeanClass.mk_smul _ (by simp)] at this
rw [ArchimedeanClass.mk_smul _ (by simp)] at this
exact this
simp_rw [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, natCast_zsmul, smul_smul, mul_comm s'.val]
