Skip to content

chore: raise priority of Grind.IntModule.OfNatModule.ofNatModule #3

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
b-mehta wants to merge 2 commits into from
+4 −0
Closed

chore: raise priority of Grind.IntModule.OfNatModule.ofNatModule #3

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a2f47a9
chore: raise priority of Grind.IntModule.OfNatModule.ofNatModule
claude May 30, 2026
559d518
chore: use priority 1100 for Grind.IntModule.OfNatModule.ofNatModule
claude May 30, 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
4 changes: 4 additions & 0 deletions Mathlib/Algebra/Group/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1088,6 +1088,10 @@ instance AddCommGroup.toGrindIntModule [s : AddCommGroup α] :
add_zsmul n m a := add_zsmul a n m
zsmul_natCast_eq_nsmul n a := by simp }

-- Give the core instance deriving a module structure from a `Grind.IntModule` a higher priority,
-- so that for an `AddCommGroup` it is preferred over the `AddCommMonoid`-based instance above.
attribute [instance 1100] Lean.Grind.IntModule.OfNatModule.ofNatModule

instance IsRightCancelAdd.toGrindAddRightCancel [AddSemigroup α] [IsRightCancelAdd α] :
Grind.AddRightCancel α where
add_right_cancel _ _ _ := add_right_cancel
Loading