Description: Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mpaacl | ⊢ ( 𝐴 ∈ 𝔸 → ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpaalem | ⊢ ( 𝐴 ∈ 𝔸 → ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) ) | |
2 | 1 | simpld | ⊢ ( 𝐴 ∈ 𝔸 → ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ) |