Documentation

Mathlib.Algebra.ModEq

Equality modulo an element #

This file defines equality modulo an element in an additive commutative monoid. In case of a group, a and b are congruent modulo p iff b - a ∈ zmultiples p.

In case of a monoid, the definition is a bit more complicated, and it is given with the use case of natural numbers in mind.

Main definitions #

See also #

SModEq is a generalisation to arbitrary submodules.

TODO #

source
def AddCommGroup.ModEq {M : Type u_1} [AddCommMonoid M] (p a b : M) :
Prop

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

If a, b are elements of an additive group, then a ≡ b [PMOD p] iff m • p = b - a for some m : ℤ, see modEq_iff_zsmul below. For additive commutative monoid, the definition is given by modEq_iff_nsmul.

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
Instances For
    source
    def AddCommGroup.«term_≡_[PMOD_]» :
    Lean.TrailingParserDescr

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

    If a, b are elements of an additive group, then a ≡ b [PMOD p] iff m • p = b - a for some m : ℤ, see modEq_iff_zsmul below. For additive commutative monoid, the definition is given by modEq_iff_nsmul.

    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
      source
      theorem AddCommGroup.modEq_iff_nsmul {M : Type u_1} [AddCommMonoid M] {a b p : M} :
      a ≡ b [PMOD p] ↔ ∃ (m : ℕ) (n : ℕ), m • p + a = n • p + b
      source
      @[simp]
      theorem AddCommGroup.modEq_refl {M : Type u_1} [AddCommMonoid M] {p : M} (a : M) :
      a ≡ a [PMOD p]
      source
      theorem AddCommGroup.modEq_rfl {M : Type u_1} [AddCommMonoid M] {a p : M} :
      a ≡ a [PMOD p]
      source
      instance AddCommGroup.instReflModEq {M : Type u_1} [AddCommMonoid M] {p : M} :
      Std.Refl (ModEq p)
      source
      theorem AddCommGroup.ModEq.symm {M : Type u_1} [AddCommMonoid M] {a b p : M} (h : a ≡ b [PMOD p]) :
      b ≡ a [PMOD p]
      source
      instance AddCommGroup.instSymmModEq {M : Type u_1} [AddCommMonoid M] {p : M} :
      Std.Symm (ModEq p)
      source
      theorem AddCommGroup.modEq_comm {M : Type u_1} [AddCommMonoid M] {a b p : M} :
      a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]
      source
      theorem AddCommGroup.ModEq.trans {M : Type u_1} [AddCommMonoid M] {a b c p : M} (hab : a ≡ b [PMOD p]) (hbc : b ≡ c [PMOD p]) :
      a ≡ c [PMOD p]
      source
      instance AddCommGroup.instIsTransModEq {M : Type u_1} [AddCommMonoid M] {p : M} :
      IsTrans M (ModEq p)
      source
      @[simp]
      theorem AddCommGroup.modEq_zero {M : Type u_1} [AddCommMonoid M] {a b : M} :
      a ≡ b [PMOD 0] ↔ a = b
      source
      @[simp]
      theorem AddCommGroup.self_modEq_zero {M : Type u_1} [AddCommMonoid M] {p : M} :
      p ≡ 0 [PMOD p]
      source
      theorem AddCommGroup.add_nsmul_modEq {M : Type u_1} [AddCommMonoid M] {a p : M} (n : ℕ) :
      a + n • p ≡ a [PMOD p]
      source
      theorem AddCommGroup.nsmul_add_modEq {M : Type u_1} [AddCommMonoid M] {a p : M} (n : ℕ) :
      n • p + a ≡ a [PMOD p]
      source
      theorem AddCommGroup.ModEq.add {M : Type u_1} [AddCommMonoid M] {a b c d p : M} (hab : a ≡ b [PMOD p]) (hcd : c ≡ d [PMOD p]) :
      a + c ≡ b + d [PMOD p]
      source
      theorem AddCommGroup.ModEq.add_left {M : Type u_1} [AddCommMonoid M] {a b p : M} (c : M) (h : a ≡ b [PMOD p]) :
      c + a ≡ c + b [PMOD p]
      source
      theorem AddCommGroup.ModEq.add_right {M : Type u_1} [AddCommMonoid M] {a b p : M} (c : M) (h : a ≡ b [PMOD p]) :
      a + c ≡ b + c [PMOD p]
      source
      theorem AddCommGroup.ModEq.of_nsmul {M : Type u_1} [AddCommMonoid M] {a b p : M} {n : ℕ} :
      a ≡ b [PMOD n • p] → a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.nsmul {M : Type u_1} [AddCommMonoid M] {a b p : M} {n : ℕ} (h : a ≡ b [PMOD p]) :
      n • a ≡ n • b [PMOD n • p]
      source
      theorem AddCommGroup.ModEq.add_nsmul {M : Type u_1} [AddCommMonoid M] {a b p : M} (n : ℕ) :
      a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.nsmul_add {M : Type u_1} [AddCommMonoid M] {a b p : M} (n : ℕ) :
      a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.map {M : Type u_1} [AddCommMonoid M] {a b p : M} {N : Type u_2} {F : Type u_3} [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (h : a ≡ b [PMOD p]) :
      f a ≡ f b [PMOD f p]
      source
      theorem AddCommGroup.map_modEq_iff {M : Type u_1} [AddCommMonoid M] {a b p : M} {N : Type u_2} {F : Type u_3} [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (hf : Function.Injective ⇑f) :
      f a ≡ f b [PMOD f p] ↔ a ≡ b [PMOD p]
      source
      @[simp]
      theorem AddCommGroup.nsmul_modEq_nsmul {M : Type u_1} [AddCommMonoid M] {a b p : M} [IsAddTorsionFree M] {n : ℕ} (hn : n ≠ 0) :
      n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.nsmul_cancel {M : Type u_1} [AddCommMonoid M] {a b p : M} [IsAddTorsionFree M] {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.

      source
      @[simp]
      theorem AddCommGroup.ModEq.add_iff_left {M : Type u_1} [AddCancelCommMonoid M] {a b c d p : M} (h : a ≡ b [PMOD p]) :
      a + c ≡ b + d [PMOD p] ↔ c ≡ d [PMOD p]
      source
      @[simp]
      theorem AddCommGroup.ModEq.add_iff_right {M : Type u_1} [AddCancelCommMonoid M] {a b c d p : M} (h : c ≡ d [PMOD p]) :
      a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.add_left_cancel {M : Type u_1} [AddCancelCommMonoid M] {a b c d p : M} (h : a ≡ b [PMOD p]) :
      a + c ≡ b + d [PMOD p] → c ≡ d [PMOD p]

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

      source
      theorem AddCommGroup.ModEq.add_right_cancel {M : Type u_1} [AddCancelCommMonoid M] {a b c d p : M} (h : c ≡ d [PMOD p]) :
      a + c ≡ b + d [PMOD p] → a ≡ b [PMOD p]

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

      source
      theorem AddCommGroup.ModEq.add_left_cancel' {M : Type u_1} [AddCancelCommMonoid M] {a b p : M} (c : M) :
      c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.add_right_cancel' {M : Type u_1} [AddCancelCommMonoid M] {a b p : M} (c : M) :
      a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p]
      source
      @[simp]
      theorem AddCommGroup.add_modEq_left {M : Type u_1} [AddCancelCommMonoid M] {a b p : M} :
      a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
      source
      @[simp]
      theorem AddCommGroup.add_modEq_right {M : Type u_1} [AddCancelCommMonoid M] {a b p : M} :
      a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]
      source
      theorem AddCommGroup.modEq_iff_zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD p] ↔ ∃ (m : ℤ), m • p = b - a
      source
      theorem AddCommGroup.modEq_iff_zsmul' {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD p] ↔ ∃ (m : ℤ), b - a = m • p
      source
      @[simp]
      theorem AddCommGroup.neg_modEq_neg {G : Type u_1} [AddCommGroup G] {p a b : G} :
      -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.of_neg {G : Type u_1} [AddCommGroup G] {p a b : G} :
      -a ≡ -b [PMOD p] → a ≡ b [PMOD p]

      Alias of the forward direction of AddCommGroup.neg_modEq_neg.

      source
      theorem AddCommGroup.ModEq.neg {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD p] → -a ≡ -b [PMOD p]

      Alias of the reverse direction of AddCommGroup.neg_modEq_neg.

      source
      @[simp]
      theorem AddCommGroup.modEq_neg {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.of_neg' {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD -p] → a ≡ b [PMOD p]

      Alias of the forward direction of AddCommGroup.modEq_neg.

      source
      theorem AddCommGroup.ModEq.neg' {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD p] → a ≡ b [PMOD -p]

      Alias of the reverse direction of AddCommGroup.modEq_neg.

      source
      theorem AddCommGroup.modEq_sub {G : Type u_1} [AddCommGroup G] (a b : G) :
      a ≡ b [PMOD b - a]
      source
      @[simp]
      theorem AddCommGroup.zsmul_modEq_zero {G : Type u_1} [AddCommGroup G] {p : G} (z : ℤ) :
      z • p ≡ 0 [PMOD p]
      source
      theorem AddCommGroup.add_zsmul_modEq {G : Type u_1} [AddCommGroup G] {p a : G} (z : ℤ) :
      a + z • p ≡ a [PMOD p]
      source
      theorem AddCommGroup.zsmul_add_modEq {G : Type u_1} [AddCommGroup G] {p a : G} (z : ℤ) :
      z • p + a ≡ a [PMOD p]
      source
      theorem AddCommGroup.ModEq.add_zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} (z : ℤ) :
      a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.zsmul_add {G : Type u_1} [AddCommGroup G] {p a b : G} (z : ℤ) :
      a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.of_zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} {z : ℤ} (h : a ≡ b [PMOD z • p]) :
      a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} {z : ℤ} (h : a ≡ b [PMOD p]) :
      z • a ≡ z • b [PMOD z • p]
      source
      @[simp]
      theorem AddCommGroup.zsmul_modEq_zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} {z : ℤ} [IsAddTorsionFree G] (hn : z ≠ 0) :
      z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.zsmul_cancel {G : Type u_1} [AddCommGroup G] {p a b : G} {z : ℤ} [IsAddTorsionFree G] (hn : z ≠ 0) :
      z • a ≡ z • b [PMOD z • p] → a ≡ b [PMOD p]

      Alias of the forward direction of AddCommGroup.zsmul_modEq_zsmul.

      source
      @[simp]
      theorem AddCommGroup.ModEq.sub_iff_left {G : Type u_1} [AddCommGroup G] {p a₁ a₂ b₁ b₂ : G} (h : a₁ ≡ b₁ [PMOD p]) :
      a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]
      source
      @[simp]
      theorem AddCommGroup.ModEq.sub_iff_right {G : Type u_1} [AddCommGroup G] {p a₁ a₂ b₁ b₂ : G} (h : a₂ ≡ b₂ [PMOD p]) :
      a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]
      source
      theorem AddCommGroup.ModEq.sub_left_cancel {G : Type u_1} [AddCommGroup G] {p a₁ a₂ b₁ b₂ : G} (h : 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.

      source
      theorem AddCommGroup.ModEq.sub {G : Type u_1} [AddCommGroup G] {p a₁ a₂ b₁ b₂ : G} (h : 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.

      source
      theorem AddCommGroup.ModEq.sub_right_cancel {G : Type u_1} [AddCommGroup G] {p a₁ a₂ b₁ b₂ : G} (h : 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.

      source
      theorem AddCommGroup.ModEq.sub_left {G : Type u_1} [AddCommGroup G] {p a b : G} (c : G) (h : a ≡ b [PMOD p]) :
      c - a ≡ c - b [PMOD p]
      source
      theorem AddCommGroup.ModEq.sub_right {G : Type u_1} [AddCommGroup G] {p a b : G} (c : G) (h : a ≡ b [PMOD p]) :
      a - c ≡ b - c [PMOD p]
      source
      theorem AddCommGroup.ModEq.sub_left_cancel' {G : Type u_1} [AddCommGroup G] {p a b : G} (c : G) :
      c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p]
      source
      theorem AddCommGroup.ModEq.sub_right_cancel' {G : Type u_1} [AddCommGroup G] {p a b : G} (c : G) :
      a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p]
      source
      theorem AddCommGroup.modEq_sub_iff_add_modEq' {G : Type u_1} [AddCommGroup G] {p a b c : G} :
      a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]
      source
      theorem AddCommGroup.modEq_sub_iff_add_modEq {G : Type u_1} [AddCommGroup G] {p a b c : G} :
      a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p]
      source
      theorem AddCommGroup.sub_modEq_iff_modEq_add' {G : Type u_1} [AddCommGroup G] {p a b c : G} :
      a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p]
      source
      theorem AddCommGroup.sub_modEq_iff_modEq_add {G : Type u_1} [AddCommGroup G] {p a b c : G} :
      a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p]
      source
      @[simp]
      theorem AddCommGroup.sub_modEq_zero {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]
      source
      theorem AddCommGroup.modEq_iff_eq_add_zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD p] ↔ ∃ (z : ℤ), b = a + z • p
      source
      theorem AddCommGroup.modEq_zero_iff_eq_zsmul {G : Type u_1} [AddCommGroup G] {p a : G} :
      a ≡ 0 [PMOD p] ↔ ∃ (z : ℤ), a = z • p
      source
      theorem AddCommGroup.not_modEq_iff_ne_add_zsmul {G : Type u_1} [AddCommGroup G] {p a b : G} :
      ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
      source
      theorem AddCommGroup.modEq_iff_eq_mod_zmultiples {G : Type u_1} [AddCommGroup G] {p a b : G} :
      a ≡ b [PMOD p] ↔ ↑a = ↑b
      source
      theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples {G : Type u_1} [AddCommGroup G] {p a b : G} :
      ¬a ≡ b [PMOD p] ↔ ↑a ≠ ↑b
      source
      theorem AddCommGroup.modEq_nsmul_cases {G : Type u_1} [AddCommGroup G] {p a b : G} (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.

      source
      theorem AddCommGroup.ModEq.nsmul_cases {G : Type u_1} [AddCommGroup G] {p a b : G} (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.

      source
      @[simp]
      theorem AddCommGroup.modEq_iff_intModEq {a b z : ℤ} :
      a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
      source
      @[deprecated AddCommGroup.modEq_iff_intModEq (since := "2026-01-13")]
      theorem AddCommGroup.modEq_iff_int_modEq {a b z : ℤ} :
      a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]

      Alias of AddCommGroup.modEq_iff_intModEq.

      source
      @[simp]
      theorem AddCommGroup.modEq_iff_natModEq {a b n : ℕ} :
      a ≡ b [PMOD n] ↔ a ≡ b [MOD n]
      source
      theorem AddCommGroup.ModEq.natCast {M : Type u_1} [AddCommMonoidWithOne M] {a b n : ℕ} (h : a ≡ b [MOD n]) :
      ↑a ≡ ↑b [PMOD ↑n]
      source
      @[simp]
      theorem AddCommGroup.natCast_modEq_natCast {M : Type u_1} [AddCommMonoidWithOne M] [CharZero M] {a b n : ℕ} :
      ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
      source
      theorem Nat.ModEq.of_natCast {M : Type u_1} [AddCommMonoidWithOne M] [CharZero M] {a b n : ℕ} :
      ↑a ≡ ↑b [PMOD ↑n] → a ≡ b [MOD n]

      Alias of the forward direction of AddCommGroup.natCast_modEq_natCast.

      source
      @[simp]
      theorem AddCommGroup.intCast_modEq_intCast {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b z : ℤ} :
      ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
      source
      @[simp]
      theorem AddCommGroup.intCast_modEq_intCast' {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b : ℤ} {n : ℕ} :
      ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]
      source
      theorem AddCommGroup.ModEq.intCast {G : Type u_1} [AddCommGroupWithOne G] [CharZero G] {a b z : ℤ} :
      a ≡ b [PMOD z] → ↑a ≡ ↑b [PMOD ↑z]

      Alias of the reverse direction of AddCommGroup.intCast_modEq_intCast.

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

      Alias of the forward direction of AddCommGroup.intCast_modEq_intCast.

      source
      @[simp]
      theorem AddCommGroup.div_modEq_div {K : Type u_1} [DivisionSemiring K] {a b c p : K} (hc : c ≠ 0) :
      a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]
      source
      @[simp]
      theorem AddCommGroup.mul_modEq_mul_right {K : Type u_1} [DivisionSemiring K] {a b c p : K} (hc : c ≠ 0) :
      a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]
      source
      @[simp]
      theorem AddCommGroup.mul_modEq_mul_left {K : Type u_1} [Semifield K] {a b c p : K} (hc : c ≠ 0) :
      c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c]