algebra.modeq

# Equality modulo an element #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 add_comm_group.modeq. Generalise smodeq to add_subgroup and redefine add_comm_group.modeq using it. Once this is done, we can rename add_comm_group.modeq to add_subgroup.modeq and multiplicativise it. Longer term, we could generalise to submonoids and also unify with nat.modeq.

def add_comm_group.modeq {α : Type u_1} (p a b : α) :
Prop

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

Equivalently (as shown in algebra.order.to_interval_mod), b does not lie in the open interval (a, a + p) modulo p, or to_Ico_mod hp a disagrees with to_Ioc_mod hp a at b, or to_Ico_div hp a disagrees with to_Ioc_div hp a at b.

Equations
Instances for add_comm_group.modeq
@[simp, refl]
theorem add_comm_group.modeq_refl {α : Type u_1} {p : α} (a : α) :
a a [PMOD p]
theorem add_comm_group.modeq_rfl {α : Type u_1} {p a : α} :
a a [PMOD p]
theorem add_comm_group.modeq_comm {α : Type u_1} {p a b : α} :
a b [PMOD p] b a [PMOD p]
@[symm]
theorem add_comm_group.modeq.symm {α : Type u_1} {p a b : α} :
a b [PMOD p] b a [PMOD p]

Alias of the forward direction of add_comm_group.modeq_comm.

@[trans]
theorem add_comm_group.modeq.trans {α : Type u_1} {p a b c : α} :
a b [PMOD p] b c [PMOD p] a c [PMOD p]
@[protected, instance]
def add_comm_group.modeq.is_refl {α : Type u_1} {p : α} :
@[simp]
theorem add_comm_group.neg_modeq_neg {α : Type u_1} {p a b : α} :
-a -b [PMOD p] a b [PMOD p]
theorem add_comm_group.modeq.neg {α : Type u_1} {p a b : α} :
a b [PMOD p] -a -b [PMOD p]

Alias of the reverse direction of add_comm_group.neg_modeq_neg.

theorem add_comm_group.modeq.of_neg {α : Type u_1} {p a b : α} :
-a -b [PMOD p] a b [PMOD p]

Alias of the forward direction of add_comm_group.neg_modeq_neg.

@[simp]
theorem add_comm_group.modeq_neg {α : Type u_1} {p a b : α} :
a b [PMOD -p] a b [PMOD p]
theorem add_comm_group.modeq.of_neg' {α : Type u_1} {p a b : α} :
a b [PMOD -p] a b [PMOD p]

Alias of the forward direction of add_comm_group.modeq_neg.

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

Alias of the reverse direction of add_comm_group.modeq_neg.

theorem add_comm_group.modeq_sub {α : Type u_1} (a b : α) :
a b [PMOD b - a]
@[simp]
theorem add_comm_group.modeq_zero {α : Type u_1} {a b : α} :
a b [PMOD 0] a = b
@[simp]
theorem add_comm_group.self_modeq_zero {α : Type u_1} {p : α} :
p 0 [PMOD p]
@[simp]
theorem add_comm_group.zsmul_modeq_zero {α : Type u_1} {p : α} (z : ) :
z p 0 [PMOD p]
theorem add_comm_group.add_zsmul_modeq {α : Type u_1} {p a : α} (z : ) :
a + z p a [PMOD p]
theorem add_comm_group.zsmul_add_modeq {α : Type u_1} {p a : α} (z : ) :
z p + a a [PMOD p]
theorem add_comm_group.add_nsmul_modeq {α : Type u_1} {p a : α} (n : ) :
a + n p a [PMOD p]
theorem add_comm_group.nsmul_add_modeq {α : Type u_1} {p a : α} (n : ) :
n p + a a [PMOD p]
@[protected]
theorem add_comm_group.modeq.add_zsmul {α : Type u_1} {p a b : α} (z : ) :
a b [PMOD p] a + z p b [PMOD p]
@[protected]
theorem add_comm_group.modeq.zsmul_add {α : Type u_1} {p a b : α} (z : ) :
a b [PMOD p] z p + a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.add_nsmul {α : Type u_1} {p a b : α} (n : ) :
a b [PMOD p] a + n p b [PMOD p]
@[protected]
theorem add_comm_group.modeq.nsmul_add {α : Type u_1} {p a b : α} (n : ) :
a b [PMOD p] n p + a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.of_zsmul {α : Type u_1} {p a b : α} {z : } :
a b [PMOD z p] a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.of_nsmul {α : Type u_1} {p a b : α} {n : } :
a b [PMOD n p] a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.zsmul {α : Type u_1} {p a b : α} {z : } :
a b [PMOD p] z a z b [PMOD z p]
@[protected]
theorem add_comm_group.modeq.nsmul {α : Type u_1} {p a b : α} {n : } :
a b [PMOD p] n a n b [PMOD n p]
@[simp]
theorem add_comm_group.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 add_comm_group.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 add_comm_group.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 add_comm_group.zsmul_modeq_zsmul.

theorem add_comm_group.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 add_comm_group.nsmul_modeq_nsmul.

@[protected, simp]
theorem add_comm_group.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])
@[protected, simp]
theorem add_comm_group.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])
@[protected, simp]
theorem add_comm_group.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])
@[protected, simp]
theorem add_comm_group.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])
@[protected]
theorem add_comm_group.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 add_comm_group.modeq.add_iff_left.

@[protected]
theorem add_comm_group.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 add_comm_group.modeq.add_iff_left.

@[protected]
theorem add_comm_group.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 add_comm_group.modeq.add_iff_right.

@[protected]
theorem add_comm_group.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 add_comm_group.modeq.sub_iff_left.

@[protected]
theorem add_comm_group.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 add_comm_group.modeq.sub_iff_left.

@[protected]
theorem add_comm_group.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 add_comm_group.modeq.sub_iff_right.

@[protected]
theorem add_comm_group.modeq.add_left {α : Type u_1} {p a b : α} (c : α) (h : a b [PMOD p]) :
c + a c + b [PMOD p]
@[protected]
theorem add_comm_group.modeq.sub_left {α : Type u_1} {p a b : α} (c : α) (h : a b [PMOD p]) :
c - a c - b [PMOD p]
@[protected]
theorem add_comm_group.modeq.add_right {α : Type u_1} {p a b : α} (c : α) (h : a b [PMOD p]) :
a + c b + c [PMOD p]
@[protected]
theorem add_comm_group.modeq.sub_right {α : Type u_1} {p a b : α} (c : α) (h : a b [PMOD p]) :
a - c b - c [PMOD p]
@[protected]
theorem add_comm_group.modeq.add_left_cancel' {α : Type u_1} {p a b : α} (c : α) :
c + a c + b [PMOD p] a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.add_right_cancel' {α : Type u_1} {p a b : α} (c : α) :
a + c b + c [PMOD p] a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.sub_left_cancel' {α : Type u_1} {p a b : α} (c : α) :
c - a c - b [PMOD p] a b [PMOD p]
@[protected]
theorem add_comm_group.modeq.sub_right_cancel' {α : Type u_1} {p a b : α} (c : α) :
a - c b - c [PMOD p] a b [PMOD p]
theorem add_comm_group.modeq_sub_iff_add_modeq' {α : Type u_1} {p a b c : α} :
a b - c [PMOD p] c + a b [PMOD p]
theorem add_comm_group.modeq_sub_iff_add_modeq {α : Type u_1} {p a b c : α} :
a b - c [PMOD p] a + c b [PMOD p]
theorem add_comm_group.sub_modeq_iff_modeq_add' {α : Type u_1} {p a b c : α} :
a - b c [PMOD p] a b + c [PMOD p]
theorem add_comm_group.sub_modeq_iff_modeq_add {α : Type u_1} {p a b c : α} :
a - b c [PMOD p] a c + b [PMOD p]
@[simp]
theorem add_comm_group.sub_modeq_zero {α : Type u_1} {p a b : α} :
a - b 0 [PMOD p] a b [PMOD p]
@[simp]
theorem add_comm_group.add_modeq_left {α : Type u_1} {p a b : α} :
a + b a [PMOD p] b 0 [PMOD p]
@[simp]
theorem add_comm_group.add_modeq_right {α : Type u_1} {p a b : α} :
a + b b [PMOD p] a 0 [PMOD p]
theorem add_comm_group.modeq_iff_eq_add_zsmul {α : Type u_1} {p a b : α} :
a b [PMOD p] (z : ), b = a + z p
theorem add_comm_group.not_modeq_iff_ne_add_zsmul {α : Type u_1} {p a b : α} :
¬a b [PMOD p] (z : ), b a + z p
theorem add_comm_group.modeq_iff_eq_mod_zmultiples {α : Type u_1} {p a b : α} :
a b [PMOD p] b = a
theorem add_comm_group.not_modeq_iff_ne_mod_zmultiples {α : Type u_1} {p a b : α} :
@[simp]
theorem add_comm_group.modeq_iff_int_modeq {a b z : } :
a b [PMOD z] a b [ZMOD z]
@[simp, norm_cast]
theorem add_comm_group.int_cast_modeq_int_cast {α : Type u_1} [char_zero α] {a b z : } :
@[simp, norm_cast]
theorem add_comm_group.nat_cast_modeq_nat_cast {α : Type u_1} [char_zero α] {a b n : } :
theorem add_comm_group.modeq.of_int_cast {α : Type u_1} [char_zero α] {a b z : } :

Alias of the forward direction of add_comm_group.int_cast_modeq_int_cast.

theorem add_comm_group.modeq.int_cast {α : Type u_1} [char_zero α] {a b z : } :

Alias of the reverse direction of add_comm_group.int_cast_modeq_int_cast.

theorem nat.modeq.of_nat_cast {α : Type u_1} [char_zero α] {a b n : } :

Alias of the forward direction of add_comm_group.nat_cast_modeq_nat_cast.

theorem add_comm_group.modeq.nat_cast {α : Type u_1} [char_zero α] {a b n : } :

Alias of the reverse direction of add_comm_group.nat_cast_modeq_nat_cast.