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 p.

See also

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} [AddCommGroup α] (p a b : α) : Prop

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.

Equations

• (a ≡ b [PMOD p]) = ∃ (z : ℤ), b - a = z • p

def AddCommGroup.«term_≡_[PMOD_]» : Lean.TrailingParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddCommGroup.modEq_refl {α : Type u_1} [AddCommGroup α] {p : α} (a : α) : a ≡ a [PMOD p]

theorem AddCommGroup.modEq_rfl {α : Type u_1} [AddCommGroup α] {p a : α} : a ≡ a [PMOD p]

theorem AddCommGroup.modEq_comm {α : Type u_1} [AddCommGroup α] {p a b : α} : a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]

theorem AddCommGroup.ModEq.symm {α : Type u_1} [AddCommGroup α] {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} [AddCommGroup α] {p a b c : α} : a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p]

instance AddCommGroup.instIsReflModEq {α : Type u_1} [AddCommGroup α] {p : α} : IsRefl α (ModEq p)

@[simp]

theorem AddCommGroup.neg_modEq_neg {α : Type u_1} [AddCommGroup α] {p a b : α} : -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.of_neg {α : Type u_1} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {p a b : α} : a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.of_neg' {α : Type u_1} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] (a b : α) : a ≡ b [PMOD b - a]

@[simp]

theorem AddCommGroup.modEq_zero {α : Type u_1} [AddCommGroup α] {a b : α} : a ≡ b [PMOD 0] ↔ a = b

@[simp]

theorem AddCommGroup.self_modEq_zero {α : Type u_1} [AddCommGroup α] {p : α} : p ≡ 0 [PMOD p]

@[simp]

theorem AddCommGroup.zsmul_modEq_zero {α : Type u_1} [AddCommGroup α] {p : α} (z : ℤ) : z • p ≡ 0 [PMOD p]

theorem AddCommGroup.add_zsmul_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (z : ℤ) : a + z • p ≡ a [PMOD p]

theorem AddCommGroup.zsmul_add_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (z : ℤ) : z • p + a ≡ a [PMOD p]

theorem AddCommGroup.add_nsmul_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (n : ℕ) : a + n • p ≡ a [PMOD p]

theorem AddCommGroup.nsmul_add_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (n : ℕ) : n • p + a ≡ a [PMOD p]

theorem AddCommGroup.ModEq.add_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} (z : ℤ) : a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p]

theorem AddCommGroup.ModEq.zsmul_add {α : Type u_1} [AddCommGroup α] {p a b : α} (z : ℤ) : a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.add_nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} (n : ℕ) : a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p]

theorem AddCommGroup.ModEq.nsmul_add {α : Type u_1} [AddCommGroup α] {p a b : α} (n : ℕ) : a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.of_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {z : ℤ} : a ≡ b [PMOD z • p] → a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.of_nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {n : ℕ} : a ≡ b [PMOD n • p] → a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {z : ℤ} : a ≡ b [PMOD p] → z • a ≡ z • b [PMOD z • p]

theorem AddCommGroup.ModEq.nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {n : ℕ} : a ≡ b [PMOD p] → n • a ≡ n • b [PMOD n • p]

@[simp]

theorem AddCommGroup.zsmul_modEq_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {z : ℤ} [NoZeroSMulDivisors ℤ α] (hn : z ≠ 0) : z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p]

@[simp]

theorem AddCommGroup.nsmul_modEq_nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {n : ℕ} [NoZeroSMulDivisors ℕ α] (hn : n ≠ 0) : n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.zsmul_cancel {α : Type u_1} [AddCommGroup α] {p a b : α} {z : ℤ} [NoZeroSMulDivisors ℤ α] (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} [AddCommGroup α] {p a b : α} {n : ℕ} [NoZeroSMulDivisors ℕ α] (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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {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} [AddCommGroup α] {p a b : α} (c : α) (h : a ≡ b [PMOD p]) : c + a ≡ c + b [PMOD p]

theorem AddCommGroup.ModEq.sub_left {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) (h : a ≡ b [PMOD p]) : c - a ≡ c - b [PMOD p]

theorem AddCommGroup.ModEq.add_right {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) (h : a ≡ b [PMOD p]) : a + c ≡ b + c [PMOD p]

theorem AddCommGroup.ModEq.sub_right {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) (h : a ≡ b [PMOD p]) : a - c ≡ b - c [PMOD p]

theorem AddCommGroup.ModEq.add_left_cancel' {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) : c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.add_right_cancel' {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) : a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.sub_left_cancel' {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) : c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p]

theorem AddCommGroup.ModEq.sub_right_cancel' {α : Type u_1} [AddCommGroup α] {p a b : α} (c : α) : a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p]

theorem AddCommGroup.modEq_sub_iff_add_modEq' {α : Type u_1} [AddCommGroup α] {p a b c : α} : a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]

theorem AddCommGroup.modEq_sub_iff_add_modEq {α : Type u_1} [AddCommGroup α] {p a b c : α} : a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p]

theorem AddCommGroup.sub_modEq_iff_modEq_add' {α : Type u_1} [AddCommGroup α] {p a b c : α} : a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p]

theorem AddCommGroup.sub_modEq_iff_modEq_add {α : Type u_1} [AddCommGroup α] {p a b c : α} : a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p]

@[simp]

theorem AddCommGroup.sub_modEq_zero {α : Type u_1} [AddCommGroup α] {p a b : α} : a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]

@[simp]

theorem AddCommGroup.add_modEq_left {α : Type u_1} [AddCommGroup α] {p a b : α} : a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

@[simp]

theorem AddCommGroup.add_modEq_right {α : Type u_1} [AddCommGroup α] {p a b : α} : a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]

theorem AddCommGroup.modEq_iff_eq_add_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} : a ≡ b [PMOD p] ↔ ∃ (z : ℤ), b = a + z • p

theorem AddCommGroup.not_modEq_iff_ne_add_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} : ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p

theorem AddCommGroup.modEq_iff_eq_mod_zmultiples {α : Type u_1} [AddCommGroup α] {p a b : α} : a ≡ b [PMOD p] ↔ ↑b = ↑a

theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples {α : Type u_1} [AddCommGroup α] {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.intCast_modEq_intCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b z : ℤ} : ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]

@[simp]

theorem AddCommGroup.intCast_modEq_intCast' {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b : ℤ} {n : ℕ} : ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]

@[simp]

theorem AddCommGroup.natCast_modEq_natCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b n : ℕ} : ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]

theorem AddCommGroup.ModEq.of_intCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b z : ℤ} : ↑a ≡ ↑b [PMOD ↑z] → a ≡ b [PMOD z]

Alias of the forward direction of AddCommGroup.intCast_modEq_intCast.

theorem AddCommGroup.ModEq.intCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b z : ℤ} : a ≡ b [PMOD z] → ↑a ≡ ↑b [PMOD ↑z]

Alias of the reverse direction of AddCommGroup.intCast_modEq_intCast.

theorem Nat.ModEq.of_natCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b n : ℕ} : ↑a ≡ ↑b [PMOD ↑n] → a ≡ b [MOD n]

Alias of the forward direction of AddCommGroup.natCast_modEq_natCast.

theorem AddCommGroup.ModEq.natCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b n : ℕ} : a ≡ b [MOD n] → ↑a ≡ ↑b [PMOD ↑n]

Alias of the reverse direction of AddCommGroup.natCast_modEq_natCast.

@[simp]

theorem AddCommGroup.div_modEq_div {α : Type u_1} [DivisionRing α] {a b c p : α} (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]

@[simp]

theorem AddCommGroup.mul_modEq_mul_right {α : Type u_1} [DivisionRing α] {a b c p : α} (hc : c ≠ 0) : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]

@[simp]

theorem AddCommGroup.mul_modEq_mul_left {α : Type u_1} [Field α] {a b c p : α} (hc : c ≠ 0) : c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c]