Theorem RingHom.charP_iff

Modification history

2025-01-08 13:31

Mathlib/Algebra/CharP/Algebra.lean

chore(Algebra/CharP/Basic): don't import `IsSimpleRing` (#20550)

Deleted RingHom.charP_iff View on Github →

2024-02-15 18:13

Mathlib/Algebra/CharP/Algebra.lean

feat(Algebra/CharP/*): add `RingHom.(charP|expChar)[_iff]` (#10574) …

Added RingHom.charP_iff View on Github →