English
If R is a normalization monoid, then the polynomial ring R[X] carries a natural normalization monoid structure, built by using the leading coefficient to form a unit and pairing it with its inverse to normalize polynomials under multiplication.
Русский
Если R — нормализационный моноид, то кольцо многочленов R[X] обладает естественной структурой нормализации моноида, строимой через ведущий коэффициент, задающий единицу, и его обратное, чтобы нормировать произведения.
LaTeX
$$$\text{If } R \text{ is a normalization monoid, then } R[X] \text{ has a natural normalization monoid structure with normUnit built from leadingCoeff.}$$$
Lean4
instance instNormalizationMonoid : NormalizationMonoid R[X]
where
normUnit
p :=
⟨C ↑(normUnit p.leadingCoeff), C ↑(normUnit p.leadingCoeff)⁻¹, by rw [← RingHom.map_mul, Units.mul_inv, C_1], by
rw [← RingHom.map_mul, Units.inv_mul, C_1]⟩
normUnit_zero := Units.ext (by simp)
normUnit_mul hp0
hq0 :=
Units.ext
(by
dsimp
rw [Ne, ← leadingCoeff_eq_zero] at *
rw [leadingCoeff_mul, normUnit_mul hp0 hq0, Units.val_mul, C_mul])
normUnit_coe_units
u :=
Units.ext
(by
dsimp
rw [← mul_one u⁻¹, Units.val_mul, Units.eq_inv_mul_iff_mul_eq]
rcases Polynomial.isUnit_iff.1 ⟨u, rfl⟩ with ⟨_, ⟨w, rfl⟩, h2⟩
rw [← h2, leadingCoeff_C, normUnit_coe_units, ← C_mul, Units.mul_inv, C_1]
rfl)
