tmohit (8e5c8361) at 14 Jul 10:19
diff file
tmohit (4316b2da) at 14 Jul 10:16
Update the file with some proofs done by Yves and definition of eig...
tmohit (81021f83) at 14 Jul 10:08
Revert "Update the file with Yves proof on conform_mx and the defin...
tmohit (c7038d67) at 14 Jul 09:45
Update the file with Yves proof on conform_mx and the definition of...
tmohit (f09a1a1d) at 13 Jul 04:00
Tried extracting eigen matrix from the definition of similar matrices.
tmohit (1a694681) at 10 Jul 11:18
Replace work_on_Jordan.v
tmohit (500c6635) at 10 Jul 10:28
Some more simplifications. Boils down to proving three lemmas on wh...
tmohit (f1617611) at 10 Jul 09:59
Simplified the proofs a bit
tmohit (c648dc40) at 09 Jul 13:52
Proved the lemma lim_sum_i
tmohit (f6303bc6) at 09 Jul 13:24
added some intermediary lemmas on limits of Jordan forms
tmohit (c4279fb7) at 06 Jul 07:36
Some progress based on the complex file in mathcomp-real-closed
tmohit (1c1a75f5) at 01 Jul 05:26
Added a comparative study with Coquelicot complex
tmohit (c8aab724) at 01 Jul 04:29
An initial version of trial
tmohit (1c30eee7) at 01 Jul 04:29
Update README.md