Commit 2025-07-22 06:11 08c479ee

View on Github →

refactor: move AddGroupWithOne instances to the Ring subfolder (#27319) There seems to be a convention here that the Algebra/Group folder should not contain things about AddMonoidWithOne, AddCommMonoidWithOne, AddGroupWithOne, and AddCommGroupWithOne, as these is more Ring-like, and cannot be additivized. I renamed the variables to R and S to match the destination files, but everything else is copied directly. Without this change, we're inconsistent and random assert_not_exists tests fail when trying to move content around within Algebra/Group.

Estimated changes

deleted theorem ULift.down_intCast
deleted theorem ULift.down_natCast
deleted theorem ULift.down_ofNat
deleted theorem ULift.up_intCast
deleted theorem ULift.up_natCast
deleted theorem ULift.up_ofNat