Commit 2024-06-08 16:29 42eb9bac

View on Github →

chore: Move CharP lemmas about order of elements (#12816) By swapping the order of imports between Algebra.CharP.Basic and GroupTheory.OrderOfElement, the first one goes from 944 dependencies to 812, and the second one from 912 to 915. Also generalise a few lemmas from semirings to non-associative semirings. This swap is justified by the fact that CharP is a purely algebraic concept while OrderOf is group-theoretic. Nevertheless, GroupTheory.OrderOfElement should be split in a future PR, in which case the CharP lemmas might move back.

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

deleted theorem CharP.addOrderOf_one

deleted theorem CharP.cast_card_eq_zero

deleted theorem charP_of_ne_zero

deleted theorem charP_of_prime_pow_injective

Modified Mathlib/Algebra/CharP/CharAndCard.lean

Modified Mathlib/Algebra/CharP/Quotient.lean

Modified Mathlib/Algebra/CharP/Two.lean

Modified Mathlib/Algebra/Module/Defs.lean

modified theorem Int.smul_one_eq_cast

modified theorem Nat.smul_one_eq_cast

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

added theorem Even.intCast

deleted theorem Int.Even.intCast

modified theorem Odd.intCast

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/Data/ZMod/Factorial.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem CharP.addOrderOf_one

added theorem Nat.cast_card_eq_zero

added theorem charP_of_ne_zero

added theorem charP_of_prime_pow_injective

Modified Mathlib/NumberTheory/Harmonic/Int.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean