Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-28 17:42 b1d8b897

View on Github →

chore(algebra/char_p): refactor char_p (#5132)

Estimated changes

modified theorem add_pow_char
modified theorem add_pow_char_of_commute
modified theorem add_pow_char_pow
modified theorem add_pow_char_pow_of_commute
modified theorem char_p.cast_card_eq_zero
added theorem char_p.congr
added theorem ring_char.dvd
modified theorem ring_char.eq
added theorem ring_char.eq_iff
added theorem ring_char.of_eq
modified theorem ring_char.spec
added theorem char_p.quotient