integer_eq — Mathlib

English

The integer subalgebra equals the infimum over valuations of the valuation subrings for each place not in S.

Русский

Подалгебра целых равна глобальной инфимумации по оценочным кольцам на местах за пределами S.

LaTeX

$$$$\\text{Set.integer}(K).toSubring = \\bigwedge_{v \\notin S} (v.valuation(K).valuationSubring).toSubring$$$$

Lean4

theorem integer_eq : (S.integer K).toSubring = ⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.toSubring :=
  SetLike.ext' <| by ext; simp

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