English
There exists b ∈ M such that the map of integerNormalization(p) under algebraMap R S equals b times p.
Русский
Существует b ∈ M, такое что отображение коэффициентов integerNormalization(p) через algebraMap R S равно b умножить на p.
LaTeX
$$$\exists b \in M, \big( (integerNormalization M p) \mapsto (algebraMap R S) \big) = (b:R) \cdot p$$$
Lean4
theorem integerNormalization_spec (p : S[X]) :
∃ b : M, ∀ i, algebraMap R S ((integerNormalization M p).coeff i) = (b : R) • p.coeff i := by
classical
use Classical.choose (exist_integer_multiples_of_finset M (p.support.image p.coeff))
intro i
rw [integerNormalization_coeff, coeffIntegerNormalization]
split_ifs with hi
·
exact
Classical.choose_spec
(Classical.choose_spec (exist_integer_multiples_of_finset M (p.support.image p.coeff)) (p.coeff i)
(Finset.mem_image.mpr ⟨i, hi, rfl⟩))
· rw [RingHom.map_zero, notMem_support_iff.mp hi, smul_zero]
