Summary
- spectrum rotation
- minor
- merge
- finished with irreducible matrix case for perron-frobenius: the maximal roots are precisely the k-th roots of unity
- order of polynomial is preserved by homomorphism
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_2.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_2.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_2.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_2.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff) |