Commit 2025-11-05 05:03 d29ce21f

View on Github →

feat({Nat,Int}/ModEq): add lemmas (#29072)

Estimated changes

Modified Mathlib/Data/Int/ModEq.lean

added theorem Int.ModEq.dvd_iff

modified theorem Int.add_modEq_left

added theorem Int.add_modEq_left_iff

modified theorem Int.add_modEq_right

added theorem Int.add_modEq_right_iff

added theorem Int.add_modulus_modEq_iff

added theorem Int.add_modulus_mul_modEq_iff

added theorem Int.add_mul_modulus_modEq_iff

added theorem Int.left_modEq_add_iff

added theorem Int.modEq_abs

modified theorem Int.modEq_add_fac

modified theorem Int.modEq_add_fac_self

added theorem Int.modEq_add_modulus_iff

added theorem Int.modEq_add_modulus_mul_iff

added theorem Int.modEq_add_mul_modulus_iff

added theorem Int.modEq_and_modEq_iff_modEq_lcm

added theorem Int.modEq_modulus_add_iff

added theorem Int.modEq_modulus_mul_add_iff

added theorem Int.modEq_mul_modulus_add_iff

added theorem Int.modEq_natAbs

added theorem Int.modEq_sub_modulus_iff

added theorem Int.modEq_sub_modulus_mul_iff

added theorem Int.modulus_add_modEq_iff

added theorem Int.modulus_modEq_zero

added theorem Int.modulus_mul_add_modEq_iff

added theorem Int.mul_modulus_add_modEq_iff

added theorem Int.right_modEq_add_iff

added theorem Int.sub_modulus_modEq_iff

added theorem Int.sub_modulus_mul_modEq_iff

Modified Mathlib/Data/Nat/ModEq.lean

added theorem Nat.ModEq.modulus_mul_add

deleted theorem Nat.ModEq.self_mul_add

modified theorem Nat.add_modEq_left

added theorem Nat.add_modEq_left_iff

modified theorem Nat.add_modEq_right

added theorem Nat.add_modEq_right_iff

added theorem Nat.add_modulus_modEq_iff

added theorem Nat.add_modulus_mul_modEq_iff

added theorem Nat.add_mul_modulus_modEq_iff

added theorem Nat.left_modEq_add_iff

added theorem Nat.modEq_add_modulus_iff

added theorem Nat.modEq_add_modulus_mul_iff

added theorem Nat.modEq_add_mul_modulus_iff

added theorem Nat.modEq_modulus_add_iff

added theorem Nat.modEq_modulus_mul_add_iff

added theorem Nat.modEq_mul_modulus_add_iff

added theorem Nat.modEq_sub_modulus_iff

added theorem Nat.modulus_add_modEq_iff

added theorem Nat.modulus_modEq_zero

added theorem Nat.modulus_mul_add_modEq_iff

added theorem Nat.mul_modulus_add_modEq_iff

added theorem Nat.right_modEq_add_iff

added theorem Nat.sub_modulus_modEq_iff