Polynomial spaces $\mathcal{P}(\mathbf{F})$, $\deg p$, $\mathcal{P}_m(\mathbf{F})$ (LADR 2.10–2.12)
- Polynomial spaces $\mathcal{P}(\mathbf{F})$, $\deg p$, $\mathcal{P}_m(\mathbf{F})$ (LADR 2.10–2.12) #Card
- $\mathcal{P}(\mathbf{F})$・次数 $\deg p$・$\mathcal{P}_m(\mathbf{F})$ の定義は？零多項式の次数は？
定義.
- $p:\mathbf{F}\to\mathbf{F}$ が多項式 $\iff$ ある $a_0,\dots,a_m\in\mathbf{F}$ で $p(z)=a_0+a_1z+\cdots+a_mz^m$（$\forall z$）。$\mathcal{P}(\mathbf{F})$ はその全体で、$\mathbf{F}^\mathbf{F}$ の部分空間。
- 次数 $\deg p=m$ $\iff$ $a_m\neq0$ の表示を持つ。恒等的に $0$ の多項式は $\deg=-\infty$ と約束。
- $\mathcal{P}_m(\mathbf{F})$＝次数 $\le m$ の多項式全体（$-\infty<m$ より $0\in\mathcal{P}_m(\mathbf{F})$）。$\mathcal{P}_m(\mathbf{F})=\operatorname{span}(1,z,\dots,z^m)$ なので有限次元。
注: 係数は多項式（関数）から一意に決まる（4.8 で証明。だから deg が well-defined）。
Polynomial F（Mathlib は係数列として定義、関数とは Polynomial.eval で接続）。Polynomial.degree（⊥ が $-\infty$ に対応）、Polynomial.degreeLE。