Theorems · Definition · group theory

AddCommGroup.ModEq

{M : Type u_1} → [AddCommMonoid M] → M → M → M → Prop

a ≡ b [PMOD p] means that b is congruent to a modulo p. If a, b are elements of an additive group, then a ≡ b [PMOD p] iff m • p = b - a for some m : ℤ, see modEq_iff_zsmul below. For additive commutative monoid, the definition is given by modEq_iff_nsmul. Equivalently (as shown in Algebra.Order.ToIntervalMod), b does not lie in the open interval (a, a + p) modulo p, or toIcoMod hp a disagrees with toIocMod hp a at b, or toIcoDiv hp a disagrees with toIocDiv hp a at b.

Defined in

Mathlib.Algebra.Group.ModEq

Cited by

107 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 31 definitions · uses no axioms

Assumes

AddCommMonoid