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 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 : α) :

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

Instances For

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.

Instances For

@[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.instIsTransModEq {α : Type u_1} [AddCommGroup α] {p : α} :

IsTrans α (ModEq 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.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.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_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 : ℤ} [IsAddTorsionFree α] (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 : ℕ} [IsAddTorsionFree α] (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 : ℤ} [IsAddTorsionFree α] (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 : ℕ} [IsAddTorsionFree α] (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 {α : 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_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_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.modEq_zero_iff_eq_zsmul {α : Type u_1} [AddCommGroup α] {p a : α} :

a ≡ 0 [PMOD p] ↔ ∃ (z : ℤ), 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] ↔ ↑a = ↑b

theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples {α : Type u_1} [AddCommGroup α] {p a b : α} :

¬a ≡ b [PMOD p] ↔ ↑a ≠ ↑b

theorem AddCommGroup.modEq_nsmul_cases {α : Type u_1} [AddCommGroup α] {p a b : α} (n : ℕ) (hn : n ≠ 0) :

a ≡ b [PMOD p] ↔ ∃ i < n, a ≡ b + i • p [PMOD n • p]

If a ≡ b [PMOD p], then mod n • p there are n cases.

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

a ≡ b [PMOD p] → ∃ i < n, a ≡ b + i • p [PMOD n • p]

Alias of the forward direction of AddCommGroup.modEq_nsmul_cases.

If a ≡ b [PMOD p], then mod n • p there are n cases.

@[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]