integerNormalization_map_to_map — Mathlib

English

The image of finsetIntegerMultiple under algebraMap equals the set of multiples of the finite set s by the common denominator.

Русский

Образ finsetIntegerMultiple через algebraMap равен множеству кратных общего знаменателя элементов множества s.

LaTeX

$$$\text{algebraMap } R S '' \text{finsetIntegerMultiple }(M,s) = \text{commonDenomOfFinset }(M,s) \cdot (s:\mathrm{Set} S)$$$

Lean4

theorem integerNormalization_map_to_map (p : S[X]) :
    ∃ b : M, (integerNormalization M p).map (algebraMap R S) = (b : R) • p :=
  let ⟨b, hb⟩ := integerNormalization_spec M p
  ⟨b,
    Polynomial.ext fun i => by
      rw [coeff_map, coeff_smul]
      exact hb i⟩

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