Commit 2025-04-04 06:20 1aa2c130

View on Github →

chore: rename primed theorem for CharP (#23656) For CharP, make use of the new feature where binder kinds of structure parameters can be precisely controlled. Now CharP.cast_eq_zero_iff is the field and CharP.cast_eq_zero_iff' is a definition.

Estimated changes

Modified Mathlib/Algebra/CharP/Algebra.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/CharP/Defs.lean

added theorem CharP.cast_eq_zero_iff'

deleted theorem CharP.cast_eq_zero_iff

Modified Mathlib/Algebra/CharP/LinearMaps.lean

Modified Mathlib/Algebra/CharP/Two.lean

Modified Mathlib/Data/Matrix/CharP.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean