English
The span of a singleton {x} equals the valuation-set {y | v(y) ≤ v(x)}.
Русский
Замкнутость множества-образа единичного множества {x} по векторной оценке равна {y | v(y) ≤ v(x)}.
LaTeX
$$(Ideal.span { x } : Set O) = {y : O | v (algebraMap O F y) ≤ v (algebraMap O F x)}$$
Lean4
theorem isIntegral_iff_v_le_one {x : R} : IsIntegral O x ↔ v x ≤ 1 :=
by
nontriviality R
have : Nontrivial O := hv.nontrivial_iff.mpr inferInstance
constructor
· rintro ⟨f, hm, hf⟩
by_cases hn : f.natDegree = 0
· rw [Polynomial.natDegree_eq_zero] at hn
obtain ⟨c, rfl⟩ := hn
simp [map_eq_zero_iff _ hv.hom_inj, hm.ne_zero_of_C] at hf
simp only [Polynomial.eval₂_eq_sum_range, Finset.sum_range_succ, hm.coeff_natDegree, map_one, one_mul,
add_eq_zero_iff_eq_neg] at hf
apply_fun v at hf
simp only [map_neg, map_pow] at hf
contrapose! hf
refine ne_of_lt (v.map_sum_lt ?_ ?_)
· simp [hn, (hf.trans' (zero_lt_one)).ne']
· simp only [Finset.mem_range, map_mul, map_pow]
intro _ hi
exact mul_lt_of_le_one_of_lt (hv.map_le_one _) <| pow_lt_pow_right₀ hf hi
· intro h
obtain ⟨y, rfl⟩ := hv.exists_of_le_one h
exact ⟨Polynomial.X - .C y, by monicity, by simp⟩
