Library companion

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import ssralg fintype perm mxpoly poly polydiv.
Require Import matrix bigop zmodp tuple.
Require Import ssrcomplements mxstructure.

This file defines companion matrices for any non-constant polynomial and prooves the properties of their characteristic and minimal polynomials companion_mx p == The companion matrix of the polynomial p.

Set Implicit Arguments.

Section Companion.

Local Open Scope ring_scope.
Import GRing.Theory.

Variable R : comRingType.

Definition companion_mxn n (p : {poly R}) :=
  \matrix_(i, j < n ) ((i == j.+1 :> nat)%:R
    - p`_i *+ ((size p).-2 == j)).

Definition companion_mx (p : {poly R}) := companion_mxn (size p).-2.+1 p.

Lemma comp_char_polyK : forall (p : {poly R}), p \is monic ->
  1 < size p -> char_poly (companion_mx p) = p.

End Companion.

Section CompanionMin.

Variable F : fieldType.
Local Open Scope ring_scope.
Import GRing.Theory.

Lemma comp_mxminpolyK : forall (p : {poly F}), p \is monic ->
  1 < size p -> mxminpoly (companion_mx p) = p.

End CompanionMin.

This page has been generated by coqdoc