Commit 2026-03-04 08:47 4e2c52aa

View on Github →

chore: split natural number lemmas from RingTheory.Radical (#36098) The new copyright headers are based on #25335.

Estimated changes

deleted theorem Nat.one_lt_radical_iff
deleted theorem Nat.radical_le_one_iff
deleted theorem Nat.radical_le_self_iff
deleted theorem Nat.radical_pos
deleted theorem Nat.two_le_radical_iff
added theorem Nat.one_lt_radical_iff
added theorem Nat.radical_le_one_iff
added theorem Nat.radical_pos
added theorem Nat.two_le_radical_iff