多項式と代数

Mathlib の多項式は Polynomial R です． 係数を埋め込む写像は Polynomial.C，不定元は Polynomial.X です．

#check Polynomial
#check Polynomial.C
#check Polynomial.X

section Polynomials

open Polynomial

variable {R : Type*} [Semiring R]

example : (X : Polynomial R) * C (1 : R) = X := by
  simp

example (a : R) : (C a : Polynomial R) + 0 = C a := by
  simp

end Polynomials

演習問題

多項式で，定数多項式の和が係数の和に対応することを示してください．

example {R : Type*} [Semiring R] (a b : R) :
    (Polynomial.C a + Polynomial.C b : Polynomial R) = Polynomial.C (a + b) := by
  -- `ext n` または `simp` を試す．
  sorry

Algebra R A は，A が R 上の代数であることを表す型クラスです． スカラー倍 r • a は，構造写像 algebraMap R A r による積として振る舞います．

#check Algebra
#check algebraMap

section Algebras

variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]

example (r : R) (a : A) : r • a = algebraMap R A r * a := by
  exact Algebra.smul_def r a

example (r s : R) : algebraMap R A (r + s) = algebraMap R A r + algebraMap R A s := by
  exact map_add (algebraMap R A) r s

end Algebras