Commit 2026-10-28 04:22 cc8d1ef7

View on Github →

feat(Algebra/CharP/Subring): generalize (#44918) Generalize some instances from concrete subfoos to arbitrary SubsemiringClass, and provide an instance SubsemiringClass.expChar.

Estimated changes

Modified Mathlib/Algebra/CharP/Subring.lean

modified theorem CharP.charP_center_iff

modified theorem ExpChar.expChar_center_iff

added theorem SubsemiringClass.charP_iff

added theorem SubsemiringClass.expChar_iff

Modified Mathlib/FieldTheory/JacobsonNoether.lean

Modified Mathlib/RingTheory/Perfection.lean