Commit 2024-05-11 02:00 4eb366ef

View on Github →

chore(Algebra/CharP/Basic): Split (#12710) Algebra.CharP.Basic currently depends on 935 files. This is unacceptably large for such a basic plain algebra file. This PR moves everything that doesn't depend on Finset (a seemingly good cut-off point) to a new file Algebra.CharP.Defs

Estimated changes

deleted theorem CharP.cast_eq_mod
deleted theorem CharP.cast_eq_zero
deleted theorem CharP.cast_eq_zero_iff
deleted theorem CharP.charP_to_charZero
deleted theorem CharP.char_ne_one
deleted theorem CharP.congr
deleted theorem CharP.eq
deleted theorem CharP.exists'
deleted theorem CharP.exists
deleted theorem CharP.exists_unique
deleted theorem CharP.intCast_eq_intCast
deleted theorem CharP.intCast_eq_zero_iff
deleted theorem CharP.natCast_eq_natCast'
deleted theorem CharP.natCast_eq_natCast
deleted theorem CharP.natCast_injOn_Iio
deleted theorem CharP.neg_one_ne_one
deleted theorem CharP.ofNat_eq_zero
deleted theorem CharP.ringChar_ne_one
deleted theorem NeZero.not_char_dvd
deleted theorem NeZero.of_not_dvd
deleted theorem RingHom.charP_iff_charP
deleted theorem ringChar.dvd
deleted theorem ringChar.eq
deleted theorem ringChar.eq_iff
deleted theorem ringChar.eq_zero
deleted theorem ringChar.of_eq
deleted theorem ringChar.spec
added theorem CharP.cast_eq_mod
added theorem CharP.cast_eq_zero
added theorem CharP.cast_eq_zero_iff
added theorem CharP.char_ne_one
added theorem CharP.congr
added theorem CharP.eq
added theorem CharP.exists'
added theorem CharP.exists_unique
added theorem CharP.neg_one_ne_one
added theorem CharP.ofNat_eq_zero
added theorem CharP.ringChar_ne_one
added theorem CharP.«exists»
added theorem NeZero.not_char_dvd
added theorem NeZero.of_not_dvd
added theorem ringChar.dvd
added theorem ringChar.eq
added theorem ringChar.eq_iff
added theorem ringChar.eq_zero
added theorem ringChar.of_eq
added theorem ringChar.spec