Theorem Nat.radical_le_self_iff

Modification history

2025-06-01 19:52

Mathlib/RingTheory/Radical.lean

feat(RingTheory/Radical): generalise and fill in TODOs (#25335) …

Added Nat.radical_le_self_iff View on Github →