instLinearOrderedAddCommGroupWithTop

English

There is an instance turning ArchimedeanClass(R) into a LinearOrderedAddCommGroupWithTop.

Русский

Существует экземпляр, превращающий ArchimedeanClass(R) в LinearOrderedAddCommGroupWithTop.

LaTeX

$$$\text{ArchimedeanClass}(R) \text{ admits a } \text{LinearOrderedAddCommGroupWithTop} \text{ structure.}$$$

Lean4

noncomputable instance : LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)
    where
  neg_top := by simp [← mk_zero, ← mk_inv]
  add_neg_cancel x
    h :=
    by
    induction x with
    | mk x
    simp [← mk_inv, ← mk_mul, mul_inv_cancel₀ (mk_eq_top_iff.not.1 h)]
  zsmul n x := n • x
  zsmul_zero'
    x := by
    induction x with
    | mk x => rw [← mk_zpow, zpow_zero, mk_one]
  zsmul_succ' := zsmul_succ'
  zsmul_neg' n
    x :=
    by
    induction x with
    | mk x
    rw [← mk_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]

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