mathlib3 documentation

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 #

See also #

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.

source
def add_comm_group.modeq {α : Type u_1} [add_comm_group α] (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
source
@[simp, refl]
theorem add_comm_group.modeq_refl {α : Type u_1} [add_comm_group α] {p : α} (a : α) :
a ≡ a [PMOD p]
source
theorem add_comm_group.modeq_rfl {α : Type u_1} [add_comm_group α] {p a : α} :
a ≡ a [PMOD p]
source
theorem add_comm_group.modeq_comm {α : Type u_1} [add_comm_group α] {p a b : α} :
a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]
source
@[symm]
theorem add_comm_group.modeq.symm {α : Type u_1} [add_comm_group α] {p a b : α} :
a ≡ b [PMOD p] → b ≡ a [PMOD p]

Alias of the forward direction of add_comm_group.modeq_comm.

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

Alias of the reverse direction of add_comm_group.neg_modeq_neg.

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

Alias of the forward direction of add_comm_group.neg_modeq_neg.

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

Alias of the forward direction of add_comm_group.modeq_neg.

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

Alias of the reverse direction of add_comm_group.modeq_neg.

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

source
theorem add_comm_group.modeq.nsmul_cancel {α : Type u_1} [add_comm_group α] {p a b : α} {n : ℕ} [no_zero_smul_divisors ℕ α] (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.

source
@[protected, simp]
theorem add_comm_group.modeq.add_iff_left {α : Type u_1} [add_comm_group α] {p a₁ a₂ b₁ b₂ : α} :
a₁ ≡ b₁ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p])
source
@[protected, simp]
theorem add_comm_group.modeq.add_iff_right {α : Type u_1} [add_comm_group α] {p a₁ a₂ b₁ b₂ : α} :
a₂ ≡ b₂ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p])
source
@[protected, simp]
theorem add_comm_group.modeq.sub_iff_left {α : Type u_1} [add_comm_group α] {p a₁ a₂ b₁ b₂ : α} :
a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p])
source
@[protected, simp]
theorem add_comm_group.modeq.sub_iff_right {α : Type u_1} [add_comm_group α] {p a₁ a₂ b₁ b₂ : α} :
a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p])
source
@[protected]
theorem add_comm_group.modeq.add_left_cancel {α : Type u_1} [add_comm_group α] {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.

source
@[protected]
theorem add_comm_group.modeq.add {α : Type u_1} [add_comm_group α] {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.

source
@[protected]
theorem add_comm_group.modeq.add_right_cancel {α : Type u_1} [add_comm_group α] {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.

source
@[protected]
theorem add_comm_group.modeq.sub {α : Type u_1} [add_comm_group α] {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.

source
@[protected]
theorem add_comm_group.modeq.sub_left_cancel {α : Type u_1} [add_comm_group α] {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.

source
@[protected]
theorem add_comm_group.modeq.sub_right_cancel {α : Type u_1} [add_comm_group α] {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.

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

Alias of the forward direction of add_comm_group.int_cast_modeq_int_cast.

source
theorem add_comm_group.modeq.int_cast {α : Type u_1} [add_comm_group_with_one α] [char_zero α] {a b z : ℤ} :
a ≡ b [PMOD z] → ↑a ≡ ↑b [PMOD ↑z]

Alias of the reverse direction of add_comm_group.int_cast_modeq_int_cast.

source
theorem nat.modeq.of_nat_cast {α : Type u_1} [add_comm_group_with_one α] [char_zero α] {a b n : ℕ} :
↑a ≡ ↑b [PMOD ↑n] → a ≡ b [MOD n]

Alias of the forward direction of add_comm_group.nat_cast_modeq_nat_cast.

source
theorem add_comm_group.modeq.nat_cast {α : Type u_1} [add_comm_group_with_one α] [char_zero α] {a b n : ℕ} :
a ≡ b [MOD n] → ↑a ≡ ↑b [PMOD ↑n]

Alias of the reverse direction of add_comm_group.nat_cast_modeq_nat_cast.