Theorem RingHom.pNilradical_le_ker_of_perfectRing

Modification history

2024-08-07 09:19
Mathlib/FieldTheory/IsPerfectClosure.lean
chore: backports for leanprover/lean4#4814 (part 28) (#15549)
Modified RingHom.pNilradical_le_ker_of_perfectRingView on Github →
2024-03-12 11:06
Mathlib/FieldTheory/IsPerfectClosure.lean
feat(FieldTheory/IsPerfectClosure): predicate `IsPerfectClosure` (#8696) …
Added RingHom.pNilradical_le_ker_of_perfectRingView on Github →