linearOrderedCommGroupWithZero — Mathlib

English

Let A be a domain with a valuation ring structure and K its fraction field. The value group ValueGroup(A,K) carries a canonical structure as a linearly ordered commutative group with zero.

Русский

Пусть A — коммутативное кольцо-домен с валюационной структурой и K — его полем дробей. Группа значений ValueGroup(A,K) естественным образом образует линейно упорядоченную коммутативную группу с нулём.

LaTeX

$$$\\operatorname{LinearOrderedCommGroupWithZero}(\\operatorname{ValueGroup}(A,K))$$$

Lean4

noncomputable instance linearOrderedCommGroupWithZero : LinearOrderedCommGroupWithZero (ValueGroup A K) :=
  { linearOrder ..,
    commGroupWithZero
      .. with
    mul_le_mul_left := by
      rintro ⟨a⟩ ⟨b⟩ ⟨c, rfl⟩ ⟨d⟩
      use c; simp only [Algebra.smul_def]; ring
    zero_le_one := ⟨0, by rw [zero_smul]⟩
    bot := 0
    bot_le := by rintro ⟨a⟩; exact ⟨0, zero_smul ..⟩ }

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