mathlib

14e7fe83 - feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship theorem (#3953)

feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship theorem (#3953) adds several assorted lemmas about matrices and `zmod p` proves that if `M` is a square matrix with entries in `zmod p`, then `tr M^p = tr M`, needed for friendship theorem Co-authored-by: Aaron Anderson <awainverse@gmail.com>