instLinearOrderedCommGroupWithZeroMrange

English

There is a canonical linear ordered group with zero structure on the range of a valuation monoid, compatible with the order coming from the value group.

Русский

Существуют естественная линейно упорядоченная группа с нулём и совместимость порядка на множество образа оценки.

LaTeX

$$$\\text{instLinearOrderedCommGroupWithZeroMrange } (v) : \\text{ LinearOrderedCommGroupWithZero } (\\mathrm{MonoidHom.mrange} v).$$$

Lean4

instance instLinearOrderedCommGroupWithZeroMrange (v : F →*₀ Γ₀) : LinearOrderedCommGroupWithZero (MonoidHom.mrange v)
    where
  __ : CommGroupWithZero (MonoidHom.mrange v) := inferInstance
  __ : LinearOrder (MonoidHom.mrange v) := inferInstance
  bot := ⟨⊥, by simp [bot_eq_zero'']⟩
  bot_le a := by simp [bot_eq_zero'', ← Subtype.coe_le_coe]
  zero_le_one := Subtype.coe_le_coe.mp zero_le_one
  mul_le_mul_left :=
    by
    simp only [Subtype.forall, MonoidHom.mem_mrange, forall_exists_index, Submonoid.mk_mul_mk, Subtype.mk_le_mk,
      forall_apply_eq_imp_iff]
    intro a b hab c
    exact mul_le_mul_left' hab (v c)

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