Skip to content

[Merged by Bors] - feat: radical lemmas for natural numbers and integers #35673

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Parcly-Taxel wants to merge 17 commits into from
+88 −20
Closed

[Merged by Bors] - feat: radical lemmas for natural numbers and integers #35673

Changes from 1 commit
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
3b2636a
feat: radical lemmas for natural numbers and integers
Parcly-Taxel Feb 23, 2026
b16c057
oops
Parcly-Taxel Feb 23, 2026
5bb0b36
mirror `Nat` lemmas for `Int`
Parcly-Taxel Feb 23, 2026
f72bc0b
`NatInt`
Parcly-Taxel Feb 23, 2026
9f23789
deprecated module
Parcly-Taxel Feb 23, 2026
d9782a6
Merge branch 'master' into radical-lemmas
Parcly-Taxel Feb 23, 2026
5652823
delete
Parcly-Taxel Feb 23, 2026
141c954
oops again
Parcly-Taxel Feb 23, 2026
0717838
fix
Parcly-Taxel Feb 23, 2026
28135ef
fix 2
Parcly-Taxel Feb 23, 2026
34d0620
Merge branch 'master' into radical-lemmas
Parcly-Taxel Feb 25, 2026
4d1444f
Merge branch 'master' into radical-lemmas
Parcly-Taxel Mar 1, 2026
a332f48
Merge branch 'master' into radical-lemmas
Parcly-Taxel Mar 4, 2026
d453413
Merge branch 'radical-lemmas' of github.com:Parcly-Taxel/mathlib4 int…
Parcly-Taxel Mar 4, 2026
bc3ac75
module deprecation
Parcly-Taxel Mar 4, 2026
4c8db8c
oops
Parcly-Taxel Mar 4, 2026
78b4420
Merge branch 'master' into radical-lemmas
Parcly-Taxel Mar 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Merge branch 'master' into radical-lemmas
  • Loading branch information
@Parcly-Taxel
Parcly-Taxel committed Mar 4, 2026
commit a332f485798ec5f5e6deab9f50fd6878d26bb653
4 changes: 2 additions & 2 deletions Mathlib/RingTheory/Radical/NatInt.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
/-
Copyright (c) 2024 Jineon Baek, Seewoo Lee. All rights reserved.
Copyright (c) 2025 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jineon Baek, Seewoo Lee, Bhavik Mehta, Arend Mellendijk
Authors: Bhavik Mehta, Arend Mellendijk
-/
module

Expand Down
You are viewing a condensed version of this merge commit. You can view the full changes here.