Summary
- merge
- slight change of definition of jordan_nf, enables lemma jordan_nf_unique
The file was modified | thys/Jordan_Normal_Form/Jordan_Normal_Form.thy (diff) |
The file was modified | thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy (diff) |
The file was modified | thys/Jordan_Normal_Form/Jordan_Normal_Form_Uniqueness.thy (diff) |
The file was modified | thys/Perron_Frobenius/Spectral_Radius_Theory_2.thy (diff) |