Commit 2024-02-15 18:13 4b36afcf

View on Github →

feat(Algebra/CharP/*): add RingHom.(charP|expChar)[_iff] (#10574) similar to RingHom.charZero[_iff]

Estimated changes

Modified Mathlib/Algebra/CharP/Algebra.lean

added theorem RingHom.charP

added theorem RingHom.charP_iff

modified theorem charP_of_injective_ringHom

modified theorem charZero_of_injective_ringHom

Modified Mathlib/Algebra/CharP/ExpChar.lean

added theorem RingHom.expChar

added theorem RingHom.expChar_iff