ofValuation

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.ofValuation

Lean4

/-- Construct a valuative relation on a ring using a valuation. -/
def ofValuation {S Γ : Type*} [CommRing S] [LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ) : ValuativeRel S
    where
  rel x y := v x ≤ v y
  rel_total x y := le_total (v x) (v y)
  rel_trans := le_trans
  rel_add hab hbc := (map_add_le_max v _ _).trans (sup_le hab hbc)
  rel_mul_right _ h := by simp only [map_mul, mul_le_mul_right' h]
  rel_mul_cancel h0
    h := by
    rw [map_zero, le_zero_iff] at h0
    simp only [map_mul] at h
    exact le_of_mul_le_mul_right h (lt_of_le_of_ne' zero_le' h0)
  not_rel_one_zero := by simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru