Theorem equiv.perm.one_lt_nonfixed_point_card_of_ne_one

feat(group_theory/perm/*): facts about the cardinality of the support of a permutation (#6951) …

feat(linear_algebra/char_poly): relates the characteristic polynomial to trace, determinant, and dimension (#3536) …