ltAddSubgroup — Mathlib

English

Membership in ltAddSubgroup corresponds exactly to valuation inequality against γ.

Русский

Членство в ltAddSubgroup эквивалентно неравенству оценки против γ.

LaTeX

$$$ x \\in \\mathrm{ltAddSubgroup}(v,\\gamma) \\iff v(x) < \\gamma $$$

Lean4

/-- The subgroup of elements whose valuation is less than a certain unit. -/
@[simps]
def ltAddSubgroup (v : Valuation R Γ₀) (γ : Γ₀ˣ) : AddSubgroup R
    where
  carrier := {x | v x < γ}
  zero_mem' := by simp
  add_mem' {x y} x_in y_in := lt_of_le_of_lt (v.map_add x y) (max_lt x_in y_in)
  neg_mem' x_in := by rwa [Set.mem_setOf, map_neg]

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