instLinearOrderedCommGroupWithZeroValueGroupWithZero

Lean4

/-- The value group-with-zero is a linearly ordered commutative group with zero. -/
instance : LinearOrderedCommGroupWithZero (ValueGroupWithZero R)
    where
  zero_le_one := bot_le
  exists_pair_ne := by
    refine ⟨0, 1, fun h => ?_⟩
    apply ge_of_eq at h
    rw [← ValueGroupWithZero.mk_zero 1, ← ValueGroupWithZero.mk_one_one, ValueGroupWithZero.mk_le_mk] at h
    simp [not_rel_one_zero] at h
  inv_zero := dif_pos .rfl
  mul_inv_cancel :=
    ValueGroupWithZero.ind fun x y h =>
      by
      rw [ne_eq, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_eq_mk] at h
      simp only [Submonoid.coe_one, mul_one, zero_mul, zero_rel, and_true] at h
      rw [ValueGroupWithZero.inv_mk x y h, ← ValueGroupWithZero.mk_one_one, ValueGroupWithZero.mk_mul_mk,
        ValueGroupWithZero.mk_eq_mk]
      simp [mul_comm]

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