lean-matrix-cookbook icon indicating copy to clipboard operation
lean-matrix-cookbook copied to clipboard

Published 20 hours ago • verified publisher icon eric-wieser

Eq 12 and Eq 18: Determinant and Trace are Product and Sum of Eigenvalues

Open MohanadAhmed opened this issue 1 year ago • 1 comments

Determinant and Trace are Product and Sum of Eigenvalues The eigenvalue as defined here is the same as the eigenvalue defined by mathlib for endomorphisms.

  1. root_charpoly_iff_has_eigenvalue and lemmas for both directions
  2. mem_eigs_iff_eigenvalue and lemmas for both directions

MohanadAhmed avatar May 30 '23 21:05 MohanadAhmed