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

• Eq (AddCommGroup.ModEq p a b) (Exists fun (z : Int) => Eq (HSub.hSub b a) (HSMul.hSMul 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.

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

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

theorem AddCommGroup.modEq_comm {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p a b) (ModEq p b a)

theorem AddCommGroup.ModEq.symm {α : Type u_1} [AddCommGroup α] {p a b : α} : ModEq p a b → ModEq p b a

Alias of the forward direction of AddCommGroup.modEq_comm.

theorem AddCommGroup.ModEq.trans {α : Type u_1} [AddCommGroup α] {p a b c : α} : ModEq p a b → ModEq p b c → ModEq p a c

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

theorem AddCommGroup.neg_modEq_neg {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p (Neg.neg a) (Neg.neg b)) (ModEq p a b)

theorem AddCommGroup.ModEq.of_neg {α : Type u_1} [AddCommGroup α] {p a b : α} : ModEq p (Neg.neg a) (Neg.neg b) → ModEq p a b

Alias of the forward direction of AddCommGroup.neg_modEq_neg.

theorem AddCommGroup.ModEq.neg {α : Type u_1} [AddCommGroup α] {p a b : α} : ModEq p a b → ModEq p (Neg.neg a) (Neg.neg b)

Alias of the reverse direction of AddCommGroup.neg_modEq_neg.

theorem AddCommGroup.modEq_neg {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq (Neg.neg p) a b) (ModEq p a b)

theorem AddCommGroup.ModEq.of_neg' {α : Type u_1} [AddCommGroup α] {p a b : α} : ModEq (Neg.neg p) a b → ModEq p a b

Alias of the forward direction of AddCommGroup.modEq_neg.

theorem AddCommGroup.ModEq.neg' {α : Type u_1} [AddCommGroup α] {p a b : α} : ModEq p a b → ModEq (Neg.neg p) a b

Alias of the reverse direction of AddCommGroup.modEq_neg.

theorem AddCommGroup.modEq_sub {α : Type u_1} [AddCommGroup α] (a b : α) : ModEq (HSub.hSub b a) a b

theorem AddCommGroup.modEq_zero {α : Type u_1} [AddCommGroup α] {a b : α} : Iff (ModEq 0 a b) (Eq a b)

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

theorem AddCommGroup.zsmul_modEq_zero {α : Type u_1} [AddCommGroup α] {p : α} (z : Int) : ModEq p (HSMul.hSMul z p) 0

theorem AddCommGroup.add_zsmul_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (z : Int) : ModEq p (HAdd.hAdd a (HSMul.hSMul z p)) a

theorem AddCommGroup.zsmul_add_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (z : Int) : ModEq p (HAdd.hAdd (HSMul.hSMul z p) a) a

theorem AddCommGroup.add_nsmul_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (n : Nat) : ModEq p (HAdd.hAdd a (HSMul.hSMul n p)) a

theorem AddCommGroup.nsmul_add_modEq {α : Type u_1} [AddCommGroup α] {p a : α} (n : Nat) : ModEq p (HAdd.hAdd (HSMul.hSMul n p) a) a

theorem AddCommGroup.ModEq.add_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} (z : Int) : ModEq p a b → ModEq p (HAdd.hAdd a (HSMul.hSMul z p)) b

theorem AddCommGroup.ModEq.zsmul_add {α : Type u_1} [AddCommGroup α] {p a b : α} (z : Int) : ModEq p a b → ModEq p (HAdd.hAdd (HSMul.hSMul z p) a) b

theorem AddCommGroup.ModEq.add_nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} (n : Nat) : ModEq p a b → ModEq p (HAdd.hAdd a (HSMul.hSMul n p)) b

theorem AddCommGroup.ModEq.nsmul_add {α : Type u_1} [AddCommGroup α] {p a b : α} (n : Nat) : ModEq p a b → ModEq p (HAdd.hAdd (HSMul.hSMul n p) a) b

theorem AddCommGroup.ModEq.of_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {z : Int} : ModEq (HSMul.hSMul z p) a b → ModEq p a b

theorem AddCommGroup.ModEq.of_nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {n : Nat} : ModEq (HSMul.hSMul n p) a b → ModEq p a b

theorem AddCommGroup.ModEq.zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {z : Int} : ModEq p a b → ModEq (HSMul.hSMul z p) (HSMul.hSMul z a) (HSMul.hSMul z b)

theorem AddCommGroup.ModEq.nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {n : Nat} : ModEq p a b → ModEq (HSMul.hSMul n p) (HSMul.hSMul n a) (HSMul.hSMul n b)

theorem AddCommGroup.zsmul_modEq_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {z : Int} [NoZeroSMulDivisors Int α] (hn : Ne z 0) : Iff (ModEq (HSMul.hSMul z p) (HSMul.hSMul z a) (HSMul.hSMul z b)) (ModEq p a b)

theorem AddCommGroup.nsmul_modEq_nsmul {α : Type u_1} [AddCommGroup α] {p a b : α} {n : Nat} [NoZeroSMulDivisors Nat α] (hn : Ne n 0) : Iff (ModEq (HSMul.hSMul n p) (HSMul.hSMul n a) (HSMul.hSMul n b)) (ModEq p a b)

theorem AddCommGroup.ModEq.zsmul_cancel {α : Type u_1} [AddCommGroup α] {p a b : α} {z : Int} [NoZeroSMulDivisors Int α] (hn : Ne z 0) : ModEq (HSMul.hSMul z p) (HSMul.hSMul z a) (HSMul.hSMul z b) → ModEq p a b

Alias of the forward direction of AddCommGroup.zsmul_modEq_zsmul.

theorem AddCommGroup.ModEq.nsmul_cancel {α : Type u_1} [AddCommGroup α] {p a b : α} {n : Nat} [NoZeroSMulDivisors Nat α] (hn : Ne n 0) : ModEq (HSMul.hSMul n p) (HSMul.hSMul n a) (HSMul.hSMul n b) → ModEq p a b

Alias of the forward direction of AddCommGroup.nsmul_modEq_nsmul.

theorem AddCommGroup.ModEq.add_iff_left {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₁ b₁ → Iff (ModEq p (HAdd.hAdd a₁ a₂) (HAdd.hAdd b₁ b₂)) (ModEq p a₂ b₂)

theorem AddCommGroup.ModEq.add_iff_right {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₂ b₂ → Iff (ModEq p (HAdd.hAdd a₁ a₂) (HAdd.hAdd b₁ b₂)) (ModEq p a₁ b₁)

theorem AddCommGroup.ModEq.sub_iff_left {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₁ b₁ → Iff (ModEq p (HSub.hSub a₁ a₂) (HSub.hSub b₁ b₂)) (ModEq p a₂ b₂)

theorem AddCommGroup.ModEq.sub_iff_right {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₂ b₂ → Iff (ModEq p (HSub.hSub a₁ a₂) (HSub.hSub b₁ b₂)) (ModEq p a₁ b₁)

theorem AddCommGroup.ModEq.add_left_cancel {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₁ b₁ → ModEq p (HAdd.hAdd a₁ a₂) (HAdd.hAdd b₁ b₂) → ModEq p a₂ b₂

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

theorem AddCommGroup.ModEq.add {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₁ b₁ → ModEq p a₂ b₂ → ModEq p (HAdd.hAdd a₁ a₂) (HAdd.hAdd b₁ b₂)

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₂ : α} : ModEq p a₂ b₂ → ModEq p (HAdd.hAdd a₁ a₂) (HAdd.hAdd b₁ b₂) → ModEq p a₁ b₁

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₂ : α} : ModEq p a₁ b₁ → ModEq p (HSub.hSub a₁ a₂) (HSub.hSub b₁ b₂) → ModEq p a₂ b₂

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

theorem AddCommGroup.ModEq.sub {α : Type u_1} [AddCommGroup α] {p a₁ a₂ b₁ b₂ : α} : ModEq p a₁ b₁ → ModEq p a₂ b₂ → ModEq p (HSub.hSub a₁ a₂) (HSub.hSub b₁ b₂)

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₂ : α} : ModEq p a₂ b₂ → ModEq p (HSub.hSub a₁ a₂) (HSub.hSub b₁ b₂) → ModEq p a₁ b₁

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 : ModEq p a b) : ModEq p (HAdd.hAdd c a) (HAdd.hAdd c b)

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

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

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

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

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

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

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

theorem AddCommGroup.modEq_sub_iff_add_modEq' {α : Type u_1} [AddCommGroup α] {p a b c : α} : Iff (ModEq p a (HSub.hSub b c)) (ModEq p (HAdd.hAdd c a) b)

theorem AddCommGroup.modEq_sub_iff_add_modEq {α : Type u_1} [AddCommGroup α] {p a b c : α} : Iff (ModEq p a (HSub.hSub b c)) (ModEq p (HAdd.hAdd a c) b)

theorem AddCommGroup.sub_modEq_iff_modEq_add' {α : Type u_1} [AddCommGroup α] {p a b c : α} : Iff (ModEq p (HSub.hSub a b) c) (ModEq p a (HAdd.hAdd b c))

theorem AddCommGroup.sub_modEq_iff_modEq_add {α : Type u_1} [AddCommGroup α] {p a b c : α} : Iff (ModEq p (HSub.hSub a b) c) (ModEq p a (HAdd.hAdd c b))

theorem AddCommGroup.sub_modEq_zero {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p (HSub.hSub a b) 0) (ModEq p a b)

theorem AddCommGroup.add_modEq_left {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p (HAdd.hAdd a b) a) (ModEq p b 0)

theorem AddCommGroup.add_modEq_right {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p (HAdd.hAdd a b) b) (ModEq p a 0)

theorem AddCommGroup.modEq_iff_eq_add_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p a b) (Exists fun (z : Int) => Eq b (HAdd.hAdd a (HSMul.hSMul z p)))

theorem AddCommGroup.not_modEq_iff_ne_add_zsmul {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (Not (ModEq p a b)) (∀ (z : Int), Ne b (HAdd.hAdd a (HSMul.hSMul z p)))

theorem AddCommGroup.modEq_iff_eq_mod_zmultiples {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (ModEq p a b) (Eq (QuotientAddGroup.mk b) (QuotientAddGroup.mk a))

theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples {α : Type u_1} [AddCommGroup α] {p a b : α} : Iff (Not (ModEq p a b)) (Ne (QuotientAddGroup.mk b) (QuotientAddGroup.mk a))

theorem AddCommGroup.modEq_iff_int_modEq {a b z : Int} : Iff (ModEq z a b) (z.ModEq a b)

theorem AddCommGroup.intCast_modEq_intCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b z : Int} : Iff (ModEq z.cast a.cast b.cast) (ModEq z a b)

theorem AddCommGroup.intCast_modEq_intCast' {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b : Int} {n : Nat} : Iff (ModEq n.cast a.cast b.cast) (ModEq n.cast a b)

theorem AddCommGroup.natCast_modEq_natCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b n : Nat} : Iff (ModEq n.cast a.cast b.cast) (n.ModEq a b)

theorem AddCommGroup.ModEq.of_intCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b z : Int} : ModEq z.cast a.cast b.cast → ModEq z a b

Alias of the forward direction of AddCommGroup.intCast_modEq_intCast.

theorem AddCommGroup.ModEq.intCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b z : Int} : ModEq z a b → ModEq z.cast a.cast b.cast

Alias of the reverse direction of AddCommGroup.intCast_modEq_intCast.

theorem Nat.ModEq.of_natCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b n : Nat} : AddCommGroup.ModEq n.cast a.cast b.cast → n.ModEq a b

Alias of the forward direction of AddCommGroup.natCast_modEq_natCast.

theorem AddCommGroup.ModEq.natCast {α : Type u_1} [AddCommGroupWithOne α] [CharZero α] {a b n : Nat} : n.ModEq a b → ModEq n.cast a.cast b.cast

Alias of the reverse direction of AddCommGroup.natCast_modEq_natCast.

theorem AddCommGroup.div_modEq_div {α : Type u_1} [DivisionRing α] {a b c p : α} (hc : Ne c 0) : Iff (ModEq p (HDiv.hDiv a c) (HDiv.hDiv b c)) (ModEq (HMul.hMul p c) a b)

theorem AddCommGroup.mul_modEq_mul_right {α : Type u_1} [DivisionRing α] {a b c p : α} (hc : Ne c 0) : Iff (ModEq p (HMul.hMul a c) (HMul.hMul b c)) (ModEq (HDiv.hDiv p c) a b)

theorem AddCommGroup.mul_modEq_mul_left {α : Type u_1} [Field α] {a b c p : α} (hc : Ne c 0) : Iff (ModEq p (HMul.hMul c a) (HMul.hMul c b)) (ModEq (HDiv.hDiv p c) a b)