# Documentation

Mathlib.Algebra.ModEq

# Equality modulo an element #

This file defines equality modulo an element in a commutative group.

## Main definitions #

• a ≡ b [PMOD p]: a and b are congruent modulo ap.

SModEq is a generalisation to arbitrary submodules.

## TODO #

Delete Int.ModEq in favour of AddCommGroup.ModEq. Generalise SModEq to AddSubgroup and redefine AddCommGroup.ModEq using it. Once this is done, we can rename AddCommGroup.ModEq to AddSubgroup.ModEq and multiplicativise it. Longer term, we could generalise to submonoids and also unify with Nat.ModEq.

def AddCommGroup.ModEq {α : Type u_1} [] (p : α) (a : α) (b : α) :

a ≡ b [PMOD p] means that b is congruent to a modulo p.

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.

Instances For
Instances For
@[simp]
theorem AddCommGroup.modEq_refl {α : Type u_1} [] {p : α} (a : α) :
a a [PMOD p]
theorem AddCommGroup.modEq_rfl {α : Type u_1} [] {p : α} {a : α} :
a a [PMOD p]
theorem AddCommGroup.modEq_comm {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD p] b a [PMOD p]
theorem AddCommGroup.ModEq.symm {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD p]b a [PMOD p]

Alias of the forward direction of AddCommGroup.modEq_comm.

theorem AddCommGroup.ModEq.trans {α : Type u_1} [] {p : α} {a : α} {b : α} {c : α} :
a b [PMOD p]b c [PMOD p]a c [PMOD p]
instance AddCommGroup.instIsReflModEq {α : Type u_1} [] {p : α} :
@[simp]
theorem AddCommGroup.neg_modEq_neg {α : Type u_1} [] {p : α} {a : α} {b : α} :
-a -b [PMOD p] a b [PMOD p]
theorem AddCommGroup.ModEq.of_neg {α : Type u_1} [] {p : α} {a : α} {b : α} :
-a -b [PMOD p]a b [PMOD p]

Alias of the forward direction of AddCommGroup.neg_modEq_neg.

theorem AddCommGroup.ModEq.neg {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD p]-a -b [PMOD p]

Alias of the reverse direction of AddCommGroup.neg_modEq_neg.

@[simp]
theorem AddCommGroup.modEq_neg {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD -p] a b [PMOD p]
theorem AddCommGroup.ModEq.of_neg' {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD -p]a b [PMOD p]

Alias of the forward direction of AddCommGroup.modEq_neg.

theorem AddCommGroup.ModEq.neg' {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD p]a b [PMOD -p]

Alias of the reverse direction of AddCommGroup.modEq_neg.

theorem AddCommGroup.modEq_sub {α : Type u_1} [] (a : α) (b : α) :
a b [PMOD b - a]
@[simp]
theorem AddCommGroup.modEq_zero {α : Type u_1} [] {a : α} {b : α} :
a b [PMOD 0] a = b
@[simp]
theorem AddCommGroup.self_modEq_zero {α : Type u_1} [] {p : α} :
p 0 [PMOD p]
@[simp]
theorem AddCommGroup.zsmul_modEq_zero {α : Type u_1} [] {p : α} (z : ) :
z p 0 [PMOD p]
theorem AddCommGroup.add_zsmul_modEq {α : Type u_1} [] {p : α} {a : α} (z : ) :
a + z p a [PMOD p]
theorem AddCommGroup.zsmul_add_modEq {α : Type u_1} [] {p : α} {a : α} (z : ) :
z p + a a [PMOD p]
theorem AddCommGroup.add_nsmul_modEq {α : Type u_1} [] {p : α} {a : α} (n : ) :
a + n p a [PMOD p]
theorem AddCommGroup.nsmul_add_modEq {α : Type u_1} [] {p : α} {a : α} (n : ) :
n p + a a [PMOD p]
theorem AddCommGroup.ModEq.add_zsmul {α : Type u_1} [] {p : α} {a : α} {b : α} (z : ) :
a b [PMOD p]a + z p b [PMOD p]
theorem AddCommGroup.ModEq.zsmul_add {α : Type u_1} [] {p : α} {a : α} {b : α} (z : ) :
a b [PMOD p]z p + a b [PMOD p]
theorem AddCommGroup.ModEq.add_nsmul {α : Type u_1} [] {p : α} {a : α} {b : α} (n : ) :
a b [PMOD p]a + n p b [PMOD p]
theorem AddCommGroup.ModEq.nsmul_add {α : Type u_1} [] {p : α} {a : α} {b : α} (n : ) :
a b [PMOD p]n p + a b [PMOD p]
theorem AddCommGroup.ModEq.of_zsmul {α : Type u_1} [] {p : α} {a : α} {b : α} {z : } :
a b [PMOD z p]a b [PMOD p]
theorem AddCommGroup.ModEq.of_nsmul {α : Type u_1} [] {p : α} {a : α} {b : α} {n : } :
a b [PMOD n p]a b [PMOD p]
theorem AddCommGroup.ModEq.zsmul {α : Type u_1} [] {p : α} {a : α} {b : α} {z : } :
a b [PMOD p]z a z b [PMOD z p]
theorem AddCommGroup.ModEq.nsmul {α : Type u_1} [] {p : α} {a : α} {b : α} {n : } :
a b [PMOD p]n a n b [PMOD n p]
@[simp]
theorem AddCommGroup.zsmul_modEq_zsmul {α : Type u_1} [] {p : α} {a : α} {b : α} {z : } [] (hn : z 0) :
z a z b [PMOD z p] a b [PMOD p]
@[simp]
theorem AddCommGroup.nsmul_modEq_nsmul {α : Type u_1} [] {p : α} {a : α} {b : α} {n : } [] (hn : n 0) :
n a n b [PMOD n p] a b [PMOD p]
theorem AddCommGroup.ModEq.zsmul_cancel {α : Type u_1} [] {p : α} {a : α} {b : α} {z : } [] (hn : z 0) :
z a z b [PMOD z p]a b [PMOD p]

Alias of the forward direction of AddCommGroup.zsmul_modEq_zsmul.

theorem AddCommGroup.ModEq.nsmul_cancel {α : Type u_1} [] {p : α} {a : α} {b : α} {n : } [] (hn : n 0) :
n a n b [PMOD n p]a b [PMOD p]

Alias of the forward direction of AddCommGroup.nsmul_modEq_nsmul.

@[simp]
theorem AddCommGroup.ModEq.add_iff_left {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ b₁ [PMOD p] → (a₁ + a₂ b₁ + b₂ [PMOD p] a₂ b₂ [PMOD p])
@[simp]
theorem AddCommGroup.ModEq.add_iff_right {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₂ b₂ [PMOD p] → (a₁ + a₂ b₁ + b₂ [PMOD p] a₁ b₁ [PMOD p])
@[simp]
theorem AddCommGroup.ModEq.sub_iff_left {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ b₁ [PMOD p] → (a₁ - a₂ b₁ - b₂ [PMOD p] a₂ b₂ [PMOD p])
@[simp]
theorem AddCommGroup.ModEq.sub_iff_right {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₂ b₂ [PMOD p] → (a₁ - a₂ b₁ - b₂ [PMOD p] a₁ b₁ [PMOD p])
theorem AddCommGroup.ModEq.add_left_cancel {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ b₁ [PMOD p]a₁ + a₂ b₁ + b₂ [PMOD p]a₂ b₂ [PMOD p]

Alias of the forward direction of AddCommGroup.ModEq.add_iff_left.

theorem AddCommGroup.ModEq.add {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ b₁ [PMOD p]a₂ b₂ [PMOD p]a₁ + a₂ b₁ + b₂ [PMOD p]

Alias of the reverse direction of AddCommGroup.ModEq.add_iff_left.

theorem AddCommGroup.ModEq.add_right_cancel {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₂ b₂ [PMOD p]a₁ + a₂ b₁ + b₂ [PMOD p]a₁ b₁ [PMOD p]

Alias of the forward direction of AddCommGroup.ModEq.add_iff_right.

theorem AddCommGroup.ModEq.sub_left_cancel {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ b₁ [PMOD p]a₁ - a₂ b₁ - b₂ [PMOD p]a₂ b₂ [PMOD p]

Alias of the forward direction of AddCommGroup.ModEq.sub_iff_left.

theorem AddCommGroup.ModEq.sub {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ b₁ [PMOD p]a₂ b₂ [PMOD p]a₁ - a₂ b₁ - b₂ [PMOD p]

Alias of the reverse direction of AddCommGroup.ModEq.sub_iff_left.

theorem AddCommGroup.ModEq.sub_right_cancel {α : Type u_1} [] {p : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₂ b₂ [PMOD p]a₁ - a₂ b₁ - b₂ [PMOD p]a₁ b₁ [PMOD p]

Alias of the forward direction of AddCommGroup.ModEq.sub_iff_right.

theorem AddCommGroup.ModEq.add_left {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) (h : a b [PMOD p]) :
c + a c + b [PMOD p]
theorem AddCommGroup.ModEq.sub_left {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) (h : a b [PMOD p]) :
c - a c - b [PMOD p]
theorem AddCommGroup.ModEq.add_right {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) (h : a b [PMOD p]) :
a + c b + c [PMOD p]
theorem AddCommGroup.ModEq.sub_right {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) (h : a b [PMOD p]) :
a - c b - c [PMOD p]
theorem AddCommGroup.ModEq.add_left_cancel' {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) :
c + a c + b [PMOD p]a b [PMOD p]
theorem AddCommGroup.ModEq.add_right_cancel' {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) :
a + c b + c [PMOD p]a b [PMOD p]
theorem AddCommGroup.ModEq.sub_left_cancel' {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) :
c - a c - b [PMOD p]a b [PMOD p]
theorem AddCommGroup.ModEq.sub_right_cancel' {α : Type u_1} [] {p : α} {a : α} {b : α} (c : α) :
a - c b - c [PMOD p]a b [PMOD p]
theorem AddCommGroup.modEq_sub_iff_add_modEq' {α : Type u_1} [] {p : α} {a : α} {b : α} {c : α} :
a b - c [PMOD p] c + a b [PMOD p]
theorem AddCommGroup.modEq_sub_iff_add_modEq {α : Type u_1} [] {p : α} {a : α} {b : α} {c : α} :
a b - c [PMOD p] a + c b [PMOD p]
theorem AddCommGroup.sub_modEq_iff_modEq_add' {α : Type u_1} [] {p : α} {a : α} {b : α} {c : α} :
a - b c [PMOD p] a b + c [PMOD p]
theorem AddCommGroup.sub_modEq_iff_modEq_add {α : Type u_1} [] {p : α} {a : α} {b : α} {c : α} :
a - b c [PMOD p] a c + b [PMOD p]
@[simp]
theorem AddCommGroup.sub_modEq_zero {α : Type u_1} [] {p : α} {a : α} {b : α} :
a - b 0 [PMOD p] a b [PMOD p]
@[simp]
theorem AddCommGroup.add_modEq_left {α : Type u_1} [] {p : α} {a : α} {b : α} :
a + b a [PMOD p] b 0 [PMOD p]
@[simp]
theorem AddCommGroup.add_modEq_right {α : Type u_1} [] {p : α} {a : α} {b : α} :
a + b b [PMOD p] a 0 [PMOD p]
theorem AddCommGroup.modEq_iff_eq_add_zsmul {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD p] z, b = a + z p
theorem AddCommGroup.not_modEq_iff_ne_add_zsmul {α : Type u_1} [] {p : α} {a : α} {b : α} :
¬a b [PMOD p] ∀ (z : ), b a + z p
theorem AddCommGroup.modEq_iff_eq_mod_zmultiples {α : Type u_1} [] {p : α} {a : α} {b : α} :
a b [PMOD p] b = a
theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples {α : Type u_1} [] {p : α} {a : α} {b : α} :
¬a b [PMOD p] b a
@[simp]
theorem AddCommGroup.modEq_iff_int_modEq {a : } {b : } {z : } :
a b [PMOD z] a b [ZMOD z]
@[simp]
theorem AddCommGroup.int_cast_modEq_int_cast {α : Type u_1} [] {a : } {b : } {z : } :
a b [PMOD z] a b [PMOD z]
@[simp]
theorem AddCommGroup.nat_cast_modEq_nat_cast {α : Type u_1} [] {a : } {b : } {n : } :
a b [PMOD n] a b [MOD n]
theorem AddCommGroup.ModEq.of_int_cast {α : Type u_1} [] {a : } {b : } {z : } :
a b [PMOD z]a b [PMOD z]

Alias of the forward direction of AddCommGroup.int_cast_modEq_int_cast.

theorem AddCommGroup.ModEq.int_cast {α : Type u_1} [] {a : } {b : } {z : } :
a b [PMOD z]a b [PMOD z]

Alias of the reverse direction of AddCommGroup.int_cast_modEq_int_cast.

theorem AddCommGroup.ModEq.nat_cast {α : Type u_1} [] {a : } {b : } {n : } :
a b [MOD n]a b [PMOD n]

Alias of the reverse direction of AddCommGroup.nat_cast_modEq_nat_cast.

theorem Nat.ModEq.of_nat_cast {α : Type u_1} [] {a : } {b : } {n : } :
a b [PMOD n]a b [MOD n]

Alias of the forward direction of AddCommGroup.nat_cast_modEq_nat_cast.