Commit 2026-03-05 11:23 83f66197

View on Github →

feat: radical lemmas for natural numbers and integers (#35673) These are needed as part of a project I'm doing for my PhD under Frank Stephan.

Estimated changes

added theorem Int.one_lt_radical_iff
added theorem Int.radical_eq_one_iff
added theorem Int.radical_le_one_iff
added theorem Int.radical_pos
added theorem Int.two_le_radical_iff
modified theorem Nat.one_lt_radical_iff
added theorem Nat.radical_eq_one_iff
modified theorem Nat.radical_le_one_iff
modified theorem Nat.radical_le_self_iff
modified theorem Nat.radical_pos
modified theorem Nat.two_le_radical_iff