English
There is a scalar-tower structure among the integer-valued subrings that makes the construction compatible with the scalar actions from the base to the extension ring.
Русский
Существует структура скалярной башни среди целочисленных подколец, обеспечивающая совместимость действий скаляров между базовым и расширенным кольцом.
LaTeX
$$$IsScalarTower(vK^{\\mathrm{integer}}, K, L)$$$
Lean4
/-- The ring of integers under a given valuation is the subring of elements with valuation ≤ 1. -/
def integer : Subring R where
carrier := {x | v x ≤ 1}
one_mem' := le_of_eq v.map_one
mul_mem' {x y} hx hy := by simp only [Set.mem_setOf_eq, map_mul, mul_le_one' hx hy]
zero_mem' := by simp only [Set.mem_setOf_eq, map_zero, zero_le']
add_mem' {x y} hx hy := le_trans (v.map_add x y) (max_le hx hy)
neg_mem' {x} hx := by simp only [Set.mem_setOf_eq] at hx; simpa only [Set.mem_setOf_eq, map_neg]
