Commit 2025-06-23 14:05 12808161

View on Github →

feat: IMO 1985 Q2 (#25783)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo1985Q2.lean

added theorem Imo1985Q2.C_mul_mod

added def Imo1985Q2.Condition

added theorem Imo1985Q2.result

Modified Mathlib.lean

Modified Mathlib/Data/Int/AbsoluteValue.lean

deleted def Int.natAbsHom

Created Mathlib/Data/Int/NatAbs.lean

added def Int.natAbsHom

added theorem Int.natAbs_natCast_sub_natCast_of_ge

added theorem Int.natAbs_natCast_sub_natCast_of_le

Modified Mathlib/Data/Nat/ModEq.lean

added theorem Nat.mod_sub_of_le

Modified Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean