English
For monomials monomial i r and monomial j s, monomial i r divides monomial j s if and only if (s = 0 or i ≤ j) and r divides s.
Русский
Для мономиалов monomial i r и monomial j s верно: monomial i r делит monomial j s тогда и только тогда, когда (s = 0 или i ≤ j) и r делит s.
LaTeX
$$$$ \\text{monomial}(i,r) \\mid \\text{monomial}(j,s) \\iff (s = 0 \\lor i \\le j) \\land (r \\mid s). $$$$
Lean4
/-- The ring isomorphism between multivariable polynomials in a single variable and
polynomials over the ground ring.
-/
@[simps]
def pUnitAlgEquiv : MvPolynomial PUnit R ≃ₐ[R] R[X]
where
toFun := eval₂ Polynomial.C fun _ => Polynomial.X
invFun := Polynomial.eval₂ MvPolynomial.C (X PUnit.unit)
left_inv :=
by
let f : R[X] →+* MvPolynomial PUnit R := Polynomial.eval₂RingHom MvPolynomial.C (X PUnit.unit)
let g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X
change ∀ p, f.comp g p = p
apply is_id
· ext a
dsimp [f, g]
rw [eval₂_C, Polynomial.eval₂_C]
· rintro ⟨⟩
dsimp [f, g]
rw [eval₂_X, Polynomial.eval₂_X]
right_inv
p :=
Polynomial.induction_on p (fun a => by rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C])
(fun p q hp hq => by rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]) fun p n _ => by
rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C, eval₂_mul, eval₂_C,
eval₂_pow, eval₂_X]
map_mul' _ _ := eval₂_mul _ _
map_add' _ _ := eval₂_add _ _
commutes' _ := eval₂_C _ _ _
