AddCommGroup.modEq_rfl
theorem AddCommGroup.modEq_rfl : ∀ {α : Type u_1} [inst : AddCommGroup α] {p a : α}, a ≡ a [PMOD p]
This theorem states that, for all elements `a` of an additive commutative group `α`, `a` is congruent to `a` modulo `p`. In mathematical terms, this means that the difference between `a` and `a`, which is zero, is divisible by `p` for any `p` in `α`. This is a fundamental property of modular arithmetic, reflecting the fact that every number is congruent to itself modulo any number.
More concisely: For all elements `a` in an additive commutative group `α`, `a` is congruent to `a` modulo any `p` in `α` (i.e., `a` is congruent to `a` mod `p`).
|
AddCommGroup.ModEq.of_neg'
theorem AddCommGroup.ModEq.of_neg' :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, a ≡ b [PMOD -p] → a ≡ b [PMOD p]
This theorem, `AddCommGroup.ModEq.of_neg'`, is an alias for the forward direction of the `AddCommGroup.modEq_neg` theorem in the context of additive commutative groups. It states that for all types `α` with `AddCommGroup` structure and for any elements `a`, `b`, and `p` of `α`, if `a` is congruent to `b` modulo `-p`, then `a` is also congruent to `b` modulo `p`. In mathematical terms, this corresponds to the fact that congruence modulo a negative number is equivalent to congruence modulo the absolute value of that number.
More concisely: If `a` is congruent to `b` modulo `-p` in an additive commutative group, then `a` is congruent to `b` modulo the absolute value of `p`.
|
AddCommGroup.modEq_iff_eq_add_zsmul
theorem AddCommGroup.modEq_iff_eq_add_zsmul :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
This theorem states that for any type `α` that forms an additive commutative group, given three elements `p`, `a`, and `b` from `α`, `a` is congruent to `b` modulo `p` if and only if there exists an integer `z` such that `b` equals `a` plus `z` times `p`. In other words, two elements `a` and `b` are congruent modulo `p` if `b` can be expressed as the sum of `a` and some multiple of `p`.
More concisely: For any additive commutative group type `α` and elements `a`, `b`, and `p` in `α`, `a` is congruent to `b` modulo `p` if and only if `b` equals `a + k * p` for some integer `k`.
|
Mathlib.Algebra.ModEq._auxLemma.35
theorem Mathlib.Algebra.ModEq._auxLemma.35 : ∀ {a b z : ℤ}, z.ModEq a b = (a ≡ b [PMOD z])
This theorem, `Mathlib.Algebra.ModEq._auxLemma.35`, states that for any three integers `a`, `b`, and `z`, the statement that `a` is equivalent to `b` modulo `z` is equivalent to the statement that `a` is equivalent to `b` taken modulo `z` in the positive mod context. In mathematical notation, we have `(a ≡ b mod z) ⇔ (a ≡ b mod+ z)`, where `mod+` is the operation of modulo in the positive context.
More concisely: The theorem `Mathlib.Algebra.ModEq._auxLemma.35` in Lean 4 states that for integers `a`, `b`, and `z`, `a` is congruent to `b` modulo `z` if and only if `a` is congruent to `b` in the positive modulo context modulo `z`.
|
AddCommGroup.intCast_modEq_intCast
theorem AddCommGroup.intCast_modEq_intCast :
∀ {α : Type u_1} [inst : AddCommGroupWithOne α] [inst_1 : CharZero α] {a b z : ℤ},
↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
This theorem states that for any type `α` that is an additive commutative group with one (i.e., has a zero and a one, addition and subtraction operations, and the addition operation is commutative), and also has a characteristic of zero, and for any integers `a`, `b`, and `z`, the statement "`a` is congruent to `b` modulo `z`" is equivalent to the statement "`a` cast to `α` is congruent to `b` cast to `α` modulo `z` cast to `α`". In other words, the congruence relationship (modulo operation) between integers is preserved even when the integers are cast to another type that has the necessary algebraic structure.
More concisely: For any additive commutative group α of characteristic zero, the congruence relation between integers is preserved under type casts: `a ≡ b (mod z)` if and only if `a.to_α ≡ b.to_α (mod z.to_α)` in α.
|
AddCommGroup.ModEq.trans
theorem AddCommGroup.ModEq.trans :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b c : α}, a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p]
This theorem states that, for any type `α` that forms an additive commutative group, the modulus operation (denoted as [PMOD p]) is transitive. In other words, for any elements `a`, `b`, `c` of the group and a modulus `p`, if `a` is equivalent to `b` modulo `p`, and `b` is equivalent to `c` modulo `p`, then `a` is equivalent to `c` modulo `p`. This is a fundamental property of the modulus operation in mathematics, expressing the fact that if two numbers leave the same remainder when divided by a number `p`, and a third number leaves the same remainder as the second when divided by `p`, then the first and third numbers also leave the same remainder when divided by `p`.
More concisely: For any additive commutative group `α` and modulus `p`, if `a ≡ b (mod p)` and `b equiv c (mod p)`, then `a ≡ c (mod p)`.
|
AddCommGroup.ModEq.zsmul_cancel
theorem AddCommGroup.ModEq.zsmul_cancel :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α} {z : ℤ} [inst_1 : NoZeroSMulDivisors ℤ α],
z ≠ 0 → z • a ≡ z • b [PMOD z • p] → a ≡ b [PMOD p]
This theorem, named `AddCommGroup.ModEq.zsmul_cancel`, is an alias for the forward direction of `AddCommGroup.zsmul_modEq_zsmul`. It states that for any type `α` which is an instance of additive commutative group, any elements `a`, `b`, and `p` of `α`, and any integer `z`, under the condition that `ℤ` (the set of integers) and `α` have no nonzero scalar multiplication divisors, if `z` is not zero and `z` multiplied by `a` is congruent to `z` multiplied by `b` modulo `z` multiplied by `p`, then `a` is congruent to `b` modulo `p`. In other words, if two elements are congruent modulo a multiple of `p` and that multiple is non-zero, we can cancel out the multiple to show that the two elements are congruent modulo `p`.
More concisely: If `α` is an additive commutative group with no nonzero scalar multiplication divisors, and `z ≠ 0` is an integer such that `z * a ≡ z * b (mod z * p)`, then `a ≡ b (mod p)`.
|
AddCommGroup.ModEq.symm
theorem AddCommGroup.ModEq.symm :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, a ≡ b [PMOD p] → b ≡ a [PMOD p]
This is an alias for the forward direction of the theorem `AddCommGroup.modEq_comm` in additive commutative groups. It states that for any type `α` that forms an additive commutative group, and for any elements `p`, `a`, and `b` of `α`, if `a` is congruent to `b` modulo `p`, then `b` is also congruent to `a` modulo `p`. In other words, the congruence relation modulo `p` is symmetric.
More concisely: If `α` is an additive commutative group and `a`, `b` are elements of `α`, then `a` is congruent to `b` modulo `p` if and only if `b` is congruent to `a` modulo `p`.
|
AddCommGroup.ModEq.sub_left_cancel
theorem AddCommGroup.ModEq.sub_left_cancel :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a₁ a₂ b₁ b₂ : α},
a₁ ≡ b₁ [PMOD p] → a₁ - a₂ ≡ b₁ - b₂ [PMOD p] → a₂ ≡ b₂ [PMOD p]
The theorem `AddCommGroup.ModEq.sub_left_cancel` is an alias of the forward direction of `AddCommGroup.ModEq.sub_iff_left`. In plain language, it states that for any type `α` that forms an additive commutative group, and for any elements `p, a₁, a₂, b₁, b₂` of `α`, if `a₁` is congruent to `b₁` modulo `p` and `a₁ - a₂` is congruent to `b₁ - b₂` modulo `p`, then `a₂` is congruent to `b₂` modulo `p`. This theorem essentially shows that in such a group, subtraction is a cancellative operation with respect to congruence modulo `p`.
More concisely: If `α` is an additive commutative group, `p` is an element of `α`, and `a₁ ≡ b₁ (mod p)` and `a₁ - a₂ ≡ b₁ - b₂ (mod p)`, then `a₂ ≡ b₂ (mod p)`.
|
AddCommGroup.ModEq.neg'
theorem AddCommGroup.ModEq.neg' :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, a ≡ b [PMOD p] → a ≡ b [PMOD -p]
This theorem, named `AddCommGroup.ModEq.neg'`, states that for any additive commutative group `α`, and any elements `p`, `a`, and `b` of `α`, if `a` is congruent to `b` modulo `p`, then `a` is also congruent to `b` modulo `-p`. In other words, if `a` and `b` have the same remainder when divided by `p`, they also have the same remainder when divided by the additive inverse of `p`. This is a variant of the theorem `AddCommGroup.modEq_neg` where the direction of implication is reversed.
More concisely: If `a` is congruent to `b` modulo `p` in an additive commutative group, then `a` is congruent to `b` modulo the additive inverse of `p`.
|
AddCommGroup.ModEq.add
theorem AddCommGroup.ModEq.add :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a₁ a₂ b₁ b₂ : α},
a₁ ≡ b₁ [PMOD p] → a₂ ≡ b₂ [PMOD p] → a₁ + a₂ ≡ b₁ + b₂ [PMOD p]
This theorem, named `AddCommGroup.ModEq.add`, states that in an additive commutative group, if two elements `a₁` and `b₁` are congruent modulo `p`, and two other elements `a₂` and `b₂` are also congruent modulo `p`, then the sum of `a₁` and `a₂` is congruent to the sum of `b₁` and `b₂` modulo `p`. This is essentially an alias of the reverse direction of the theorem `AddCommGroup.ModEq.add_iff_left`.
More concisely: In an additive commutative group, if `a₁ ≡ b₁` and `a₂ ≡ b₂` are congruences modulo `p`, then `(a₁ + a₂) ≡ (b₁ + b₂)` modulo `p`.
|
AddCommGroup.ModEq.sub_right_cancel
theorem AddCommGroup.ModEq.sub_right_cancel :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a₁ a₂ b₁ b₂ : α},
a₂ ≡ b₂ [PMOD p] → a₁ - a₂ ≡ b₁ - b₂ [PMOD p] → a₁ ≡ b₁ [PMOD p]
This theorem, `AddCommGroup.ModEq.sub_right_cancel`, is an alias for the forward direction of `AddCommGroup.ModEq.sub_iff_right` in Lean. It states that for any type `α` which forms an additive commutative group, given any elements `p`, `a₁`, `a₂`, `b₁`, and `b₂` of `α`, if `a₂` is congruent to `b₂` modulo `p` and `a₁` minus `a₂` is congruent to `b₁` minus `b₂` modulo `p`, then `a₁` is congruent to `b₁` modulo `p`. In simpler terms, if two numbers have the same remainder when divided by `p`, and the difference between each of these numbers and another pair of numbers also have the same remainder when divided by `p`, then the first pair of numbers are congruent modulo `p`.
More concisely: If `a₁ ≡ b₁ (mod p)` and `a₂ ≡ b₂ (mod p)` imply `a₁ - a₂ ≡ b₁ - b₂ (mod p)`, then `a₁ ≡ b₁ (mod p)`.
|
AddCommGroup.modEq_comm
theorem AddCommGroup.modEq_comm :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]
This theorem states that for any type `α` that is an instance of an additive commutative group, and for any elements `p`, `a`, and `b` in this group, the congruence `a` is congruent to `b` modulo `p` is equivalent to `b` being congruent to `a` modulo `p`. In simpler terms, the order of `a` and `b` does not matter when we are checking for their congruence modulo `p` in an additive commutative group.
More concisely: In an additive commutative group, the congruences of two elements are equal modulo a third element if and only if the elements are congruent to each other modulo that element.
|
AddCommGroup.ModEq.sub
theorem AddCommGroup.ModEq.sub :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a₁ a₂ b₁ b₂ : α},
a₁ ≡ b₁ [PMOD p] → a₂ ≡ b₂ [PMOD p] → a₁ - a₂ ≡ b₁ - b₂ [PMOD p]
This theorem, named `AddCommGroup.ModEq.sub`, states that in an additive commutative group, if two elements `a₁` and `b₁` are congruent modulo `p`, and two other elements `a₂` and `b₂` are also congruent modulo `p`, then the difference `a₁ - a₂` is congruent to the difference `b₁ - b₂` modulo `p`. In other words, the congruence relation modulo `p` is preserved under subtraction in an additive commutative group.
More concisely: In an additive commutative group, if `a₁ ≡ b₁` and `a₂ ≡ b₂` are congruences modulo `p`, then `(a₁ - a₂) ≡ (b₁ - b₂)` modulo `p`.
|
AddCommGroup.ModEq.neg
theorem AddCommGroup.ModEq.neg :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, a ≡ b [PMOD p] → -a ≡ -b [PMOD p]
This theorem, named `AddCommGroup.ModEq.neg`, is an alias of the reverse direction of another theorem `AddCommGroup.neg_modEq_neg`. It states that for any type `α` that has an additive commutative group structure, and for any elements `p`, `a`, and `b` of this type, if `a` is congruent to `b` modulo `p`, then `-a` (the additive inverse of `a`) is also congruent to `-b` (the additive inverse of `b`) modulo `p`.
More concisely: For all additive commutative groups `α`, and elements `a`, `b`, and `p` of `α`, if `a` is congruent to `b` modulo `p`, then `-a` is congruent to `-b` modulo `p`.
|
AddCommGroup.ModEq.nsmul_cancel
theorem AddCommGroup.ModEq.nsmul_cancel :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α} {n : ℕ} [inst_1 : NoZeroSMulDivisors ℕ α],
n ≠ 0 → n • a ≡ n • b [PMOD n • p] → a ≡ b [PMOD p]
This theorem, named `AddCommGroup.ModEq.nsmul_cancel`, is an alias of the forward direction of `AddCommGroup.nsmul_modEq_nsmul`. It states that for any type `α` that is an additive commutative group, and for any elements `p`, `a`, and `b` of `α`, and any natural number `n`, assuming that no zero scalar multiplication divisors exist for `ℕ` and `α`, if `n` is not zero and `n • a` and `n • b` are congruent modulo `n • p`, then `a` and `b` are congruent modulo `p`. Here `n • a` and `n • b` denote the results of scalar multiplication of `a` and `b` by `n` respectively.
More concisely: If `α` is an additive commutative group with no zero scalar multiplication divisors, and `n` is a non-zero natural number such that `n • a ≡ n • b (mod n • p)`, then `a ≡ b (mod p)`.
|
AddCommGroup.ModEq.add_right_cancel
theorem AddCommGroup.ModEq.add_right_cancel :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a₁ a₂ b₁ b₂ : α},
a₂ ≡ b₂ [PMOD p] → a₁ + a₂ ≡ b₁ + b₂ [PMOD p] → a₁ ≡ b₁ [PMOD p]
This theorem, `AddCommGroup.ModEq.add_right_cancel`, is an alias of the forward direction of `AddCommGroup.ModEq.add_iff_right`. It states that for any type `α` that forms an additive commutative group, given elements `a₁, a₂, b₁, b₂` and `p` of `α`, if `a₂` is congruent to `b₂` modulo `p` and `a₁ + a₂` is congruent to `b₁ + b₂` modulo `p`, then `a₁` must be congruent to `b₁` modulo `p`. In mathematical notation, it states that if $a_2 \equiv b_2 \pmod{p}$ and $a_1 + a_2 \equiv b_1 + b_2 \pmod{p}$, then $a_1 \equiv b_1 \pmod{p}$. This theorem essentially allows cancellation to occur when working with congruences in an additive commutative group.
More concisely: If `α` is an additive commutative group, `a₁ ≡ b₁ (mod p)`, `a₂ ≡ b₂ (mod p)`, and `a₁ + a₂ ≡ b₁ + b₂ (mod p)`, then `a₁ ≡ b₁ (mod p)`.
|
AddCommGroup.ModEq.add_left_cancel
theorem AddCommGroup.ModEq.add_left_cancel :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a₁ a₂ b₁ b₂ : α},
a₁ ≡ b₁ [PMOD p] → a₁ + a₂ ≡ b₁ + b₂ [PMOD p] → a₂ ≡ b₂ [PMOD p]
This is a theorem about modular arithmetic in an additive commutative group. The theorem, named `AddCommGroup.ModEq.add_left_cancel`, states that for any type `α` which forms an additive commutative group, and any elements `p`, `a₁`, `a₂`, `b₁`, and `b₂` of `α`, if `a₁` is congruent to `b₁` modulo `p` and the sum of `a₁` and `a₂` is congruent to the sum of `b₁` and `b₂` modulo `p`, then `a₂` is congruent to `b₂` modulo `p`. In other words, it states that in a modular arithmetic context, if two pairs of elements have the same sum modulo `p`, and one element in each pair is congruent modulo `p`, then the other elements in the pairs are also congruent modulo `p`.
More concisely: If `a₁ ≡ b₁ (mod p)` and `a₁ + a₂ ≡ b₁ + b₂ (mod p)`, then `a₂ ≡ b₂ (mod p)` in an additive commutative group.
|
Mathlib.Algebra.ModEq._auxLemma.34
theorem Mathlib.Algebra.ModEq._auxLemma.34 : ∀ {a b n : ℕ}, n.ModEq a b = (↑n).ModEq ↑a ↑b
This theorem states that for any three natural numbers `a`, `b`, and `n`, the statement "`a` is congruent to `b` modulo `n`" is equivalent to the statement "the integer representation of `a` is congruent to the integer representation of `b` modulo the integer representation of `n`". Essentially, it's saying that the modulo operation behaves the same way whether you're working with natural numbers or integers.
More concisely: For natural numbers `a`, `b`, and `n`, `a` is congruent to `b` modulo `n` if and only if the integer representations of `a` and `b` are congruent modulo the integer representation of `n`.
|
Mathlib.Algebra.ModEq._auxLemma.2
theorem Mathlib.Algebra.ModEq._auxLemma.2 : ∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, (a = -b) = (-a = b)
This theorem, `Mathlib.Algebra.ModEq._auxLemma.2`, states that for any type `G` that has an involutive negation operation (i.e., negating twice gives the original element), and any two elements `a` and `b` of this type, `a` being equal to the negation of `b` is the same as the negation of `a` being equal to `b`. In other words, it specifies a symmetry property of the negation operation in such algebraic structures.
More concisely: For any type `G` with an involutive negation operation, the equality of `a` and the negation of `b` is equivalent to the equality of the negation of `a` and `b`.
|
Mathlib.Algebra.ModEq._auxLemma.31
theorem Mathlib.Algebra.ModEq._auxLemma.31 :
∀ {α : Type u_1} [inst : AddCommGroupWithOne α] (m n : ℤ), m • ↑n = ↑(m * n)
This theorem, known as `_auxLemma.31` from the `Mathlib.Algebra.ModEq` module, asserts that for any type `α` that has the structure of an additive commutative group along with an identity element for multiplication, and for any integers `m` and `n`, the action of scaling `n` by `m` has the same effect as multiplying `m` and `n` together and then converting the result to `α`. In mathematical notation, this is stated as `m • ↑n = ↑(m * n)`.
More concisely: For any additive commutative group `α` with an identity element for multiplication, scaling an integer `n` by another integer `m` is equivalent to multiplying `m` and `n` and then converting the result to the group `α`, i.e., `m • ↑n = ↑(m * n)`.
|
AddCommGroup.ModEq.of_neg
theorem AddCommGroup.ModEq.of_neg :
∀ {α : Type u_1} [inst : AddCommGroup α] {p a b : α}, -a ≡ -b [PMOD p] → a ≡ b [PMOD p]
This theorem, "AddCommGroup.ModEq.of_neg", is an alias of the forward direction of "AddCommGroup.neg_modEq_neg". The theorem states that for any type 'α' that has an instance of an additive commutative group, given any three elements 'p', 'a', and 'b' of type 'α', if '-a' is congruent to '-b' modulo 'p', then 'a' is also congruent to 'b' modulo 'p'. Essentially, it ensures the preservation of congruence under negation in the context of an additive commutative group.
More concisely: If '-a' is congruent to '-b' modulo p in an additive commutative group, then a is congruent to b modulo p.
|