Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-29 17:36 14e7fe83

View on Github →

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

Estimated changes

modified theorem add_pow_char
added theorem add_pow_char_pow
added theorem iterate_frobenius
added theorem sub_pow_char
added theorem sub_pow_char_pow
added theorem matrix.map_sub
added theorem matrix.scalar_inj
added theorem polynomial.commute_X
added theorem finite_field.pow_card
added theorem zmod.card_units
added theorem zmod.expand_card
added theorem zmod.pow_card
added theorem polynomial.expand_char
added theorem polynomial.map_expand
added theorem zmod.trace_pow_card
deleted theorem zmod.card_units
deleted theorem zmod.fermat_little
deleted theorem zmod.fermat_little_units