Commit 2025-03-29 19:12 275282a1

View on Github →

feat: ZMod.val ofNat(a) (#23441) Also make n explicit in ZMod.val_natCast. Zulip

Estimated changes

modified theorem ZMod.val_natCast
modified theorem ZMod.val_natCast_of_lt
added theorem ZMod.val_ofNat
added theorem ZMod.val_ofNat_of_lt