Mathlib.Algebra.Group.Prod._auxLemma.1
theorem Mathlib.Algebra.Group.Prod._auxLemma.1 :
∀ {M : Type u_5} {N : Type u_6} [inst : One M] [inst_1 : One N] {x : M} {y : N}, ((x, y) = 1) = (x = 1 ∧ y = 1)
This theorem, from the Mathematical Library Algebra Group section, states that for any types `M` and `N` that have an associated identity element (`One M` and `One N`, respectively), the tuple `(x, y)` where `x` is an element of `M` and `y` is an element of `N`, is equal to the identity element `1` if and only if both `x` and `y` are equal to their respective identity elements. In essence, this theorem is making a statement about the nature of the identity element in a product space.
More concisely: For any types `M` and `N` with identity elements `One M` and `One N`, respectively, the tuple `(x, y)` is equal to the identity element `(One M, One N)` if and only if `x = One M` and `y = One N`.
|
Prod.mk_mul_mk
theorem Prod.mk_mul_mk :
∀ {M : Type u_5} {N : Type u_6} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
This theorem, `Prod.mk_mul_mk`, states that for any types `M` and `N` that have multiplication defined on them, the multiplication of two pairs, `(a₁, b₁)` and `(a₂, b₂)`, is equivalent to the pair of their respective multiplications, `(a₁ * a₂, b₁ * b₂)`. In mathematical terms, given two pairs from the cartesian product of `M` and `N`, their product is the pair made by multiplying the first elements together and then the second elements together.
More concisely: For types `M` and `N` with multiplication, `(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)`.
|
Prod.mk_add_mk
theorem Prod.mk_add_mk :
∀ {M : Type u_5} {N : Type u_6} [inst : Add M] [inst_1 : Add N] (a₁ a₂ : M) (b₁ b₂ : N),
(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
This theorem, `Prod.mk_add_mk`, states that for any two types `M` and `N` that have an addition operation defined, the sum of pairs of elements from these types behaves as expected. Specifically, the sum of the pair `(a₁, b₁)` and `(a₂, b₂)` is equal to the pair `(a₁ + a₂, b₁ + b₂)`, where `a₁` and `a₂` are elements of type `M`, and `b₁` and `b₂` are elements of type `N`. This means that the addition operation is applied component-wise on the elements of the pairs.
More concisely: For types `M` and `N` with addition operations, the operation `(+)` on pairs `(a, b)` from `M × N` is defined as `(a + a', b + b')` where `a` and `a'` are from `M` and `b` and `b'` are from `N`.
|
Prod.fst_mul_snd
theorem Prod.fst_mul_snd :
∀ {M : Type u_5} {N : Type u_6} [inst : MulOneClass M] [inst_1 : MulOneClass N] (p : M × N),
(p.1, 1) * (1, p.2) = p
The theorem `Prod.fst_mul_snd` states that for any types `M` and `N` which have a multiplication and an identity operation (i.e., they are members of the `MulOneClass`), and for any pair `p` of type `M × N`, the product of the pair `(p.1, 1)` and `(1, p.2)` is equal to `p`. Here, `p.1` and `p.2` denote the first and second elements of the pair `p`, respectively. In other words, the multiplication operation distributes over the elements of the pair in a way that the identity elements do not affect the result.
More concisely: For any types `M` and `N` in the `MulOneClass` and any `(m, n)` in `M × N`, `(m, 1) * (1, n) = (m, n)`.
|
Mathlib.Algebra.Group.Prod._auxLemma.2
theorem Mathlib.Algebra.Group.Prod._auxLemma.2 :
∀ {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : Zero N] {x : M} {y : N}, ((x, y) = 0) = (x = 0 ∧ y = 0)
This theorem, `Mathlib.Algebra.Group.Prod._auxLemma.2`, states that for any types `M` and `N` that have zero elements, and any elements `x` of type `M` and `y` of type `N`, the pair `(x, y)` is equivalent to zero if and only if both `x` and `y` are zero. In other words, a pair of elements from two types with zero elements is considered zero if both elements in the pair are individually zero.
More concisely: For types `M` and `N` with zero elements, `(x, y) = (0 : M) × (0 : N)` if and only if `x = 0` and `y = 0`.
|