Commit 2023-06-02 16:45 22a37712

View on Github →

feat: port LinearAlgebra.Matrix.Charpoly.FiniteField (#4601)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

added theorem FiniteField.Matrix.charpoly_pow_card

added theorem FiniteField.trace_pow_card

added theorem ZMod.charpoly_pow_card

added theorem ZMod.trace_pow_card