IsSquare.exists_sq
theorem IsSquare.exists_sq : ∀ {α : Type u_2} [inst : Monoid α] (m : α), IsSquare m → ∃ c, m = c ^ 2
This theorem, referred to as an alias of the forward direction of `isSquare_iff_exists_sq`, states that for any type `α` with a multiplication operation (a monoid), given an element `m` of that type, if `m` is a square (according to the `IsSquare` definition, meaning that there exists some `r` such that `m = r * r`), then there exists a `c` such that `m` is equal to `c` raised to the power of 2.
More concisely: If `m` is a square in a monoid `α` with multiplication operation, then there exists `c` such that `m = c^2`.
|
Odd.neg
theorem Odd.neg : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd a → Odd (-a)
The theorem `Odd.neg` states that for any type `α` that is a ring, if an element `a` of `α` is odd (i.e., there exists a number `k` such that `a` equals `2*k + 1`), then the negative of `a` (denoted as `-a`) is also odd. In other words, the negation of an odd number in a ring is also an odd number.
More concisely: If `a` is an odd element in a ring `α`, then `-a` is also an odd element.
|
odd_one
theorem odd_one : ∀ {α : Type u_2} [inst : Semiring α], Odd 1
The theorem `odd_one` states that, for any type `α` that forms a semiring, the number 1 is odd. In more mathematical terms, this means that there exists a number `k` such that `1 = 2*k + 1`, which is the definition of an odd number in the given semiring.
More concisely: In a semiring, the multiplicative identity is an odd element.
|
even_two
theorem even_two : ∀ {α : Type u_2} [inst : Semiring α], Even 2
The theorem `even_two` states that for all types `α` equipped with a semiring structure, the number 2 is even. In the context of the defined property `Even`, this means that there exists a number `r` in `α` such that `2 = r + r`.
More concisely: In any semiring, 2 is equal to the sum of two identical elements.
|
Odd.add_odd
theorem Odd.add_odd : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Odd a → Odd b → Even (a + b)
The theorem `Odd.add_odd` states that for any type `α` that is a semiring, given two elements `m` and `n` of that semiring, if `m` and `n` are both odd, then their sum `m + n` is even. In other words, the sum of two odd numbers is always even in any semiring.
More concisely: If `m` and `n` are odd elements of a semiring, then their sum `m + n` is even.
|
Odd.neg_one_pow
theorem Odd.neg_one_pow :
∀ {α : Type u_2} [inst : Monoid α] [inst_1 : HasDistribNeg α] {n : ℕ}, Odd n → (-1) ^ n = -1
The theorem `Odd.neg_one_pow` states that for any natural number `n` in a monoid structure `α` (which is also endowed with an operation `HasDistribNeg`), if `n` is an odd number (meaning there exists an integer `k` such that `n` is equal to `2k + 1`), then the expression `(-1) ^ n` is equal to `-1`. In other words, raising `-1` to the power of any odd natural number results in `-1`.
More concisely: For any monoid `α` with `HasDistribNeg`, if `n` is an odd natural number, then `(-1) ^ n = -1`.
|
Odd.strictMono_pow
theorem Odd.strictMono_pow :
∀ {R : Type u_4} [inst : LinearOrderedSemiring R] [inst_1 : ExistsAddOfLE R] {n : ℕ},
Odd n → StrictMono fun a => a ^ n
The theorem `Odd.strictMono_pow` states that for any type `R` that forms a linearly ordered ring, and for any natural number `n` such that `n` is odd, the function `f(a) = a^n` is strictly monotonic. In other words, if `n` is an odd natural number and `a` and `b` are elements from a linearly ordered ring such that `a < b`, then `a^n < b^n`.
More concisely: For any odd natural number `n` and linearly ordered ring `R`, the function `a ↦ a^n` is strictly increasing on `R`.
|
Even.map
theorem Even.map :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
[inst_2 : FunLike F α β] [inst_3 : AddMonoidHomClass F α β] {m : α} (f : F), Even m → Even (f m)
The theorem `Even.map` states that for all types `F`, `α`, and `β`, where `α` and `β` are types with addition and zero (`AddZeroClass`), `F` is a type that can be injectively coerced into a function from `α` to `β` (`FunLike F α β`), and `F` is an additive monoid homomorphism from `α` to `β` (`AddMonoidHomClass F α β`), if a value `m` of type `α` is even (i.e., it can be expressed as `r + r` for some `r`), then the result of applying a function `f` of type `F` to `m` is also even. In other words, the image under an additive monoid homomorphism of an even element from an additive monoid is also even.
More concisely: If `F` is an additive monoid homomorphism from an additive monoid `α` to an additive monoid `β`, then for all even `m` in `α`, `F(m)` is even in `β`.
|
isSquare_op_iff
theorem isSquare_op_iff : ∀ {α : Type u_2} [inst : Mul α] {a : α}, IsSquare (MulOpposite.op a) ↔ IsSquare a
This theorem states that for any type `α` that has a multiplication operation, and for any element `a` of that type, `a` is a square in the multiplicative sense (i.e., there exists an `r` in `α` such that `a = r * r`) if and only if the multiplicative opposite of `a` is also a square. In other words, an element and its multiplicative opposite share the property of being a square.
More concisely: For any type `α` with multiplication and any `a` in `α`, `a` and its multiplicative opposite are both squares if and only if they have a common square root in `α`.
|
Even.exists_bit0
theorem Even.exists_bit0 : ∀ {α : Type u_2} [inst : Add α] {a : α}, Even a → ∃ b, a = bit0 b
This theorem, named "Even.exists_bit0", states that for any type 'α' that has an addition operation defined, if an element 'a' of type 'α' is even (i.e., it can be expressed as the sum of two identical elements), then there exists another element 'b' such that 'a' is equal to twice 'b'. The theorem is an alias of the forward direction of another theorem, 'even_iff_exists_bit0'.
More concisely: If an element `a` of type `α` with an addition operation is even, then there exists an element `b` such that `a = 2 * b`.
|
Odd.neg_pow
theorem Odd.neg_pow :
∀ {α : Type u_2} [inst : Monoid α] [inst_1 : HasDistribNeg α] {n : ℕ}, Odd n → ∀ (a : α), (-a) ^ n = -a ^ n := by
sorry
The theorem `Odd.neg_pow` states that for any type `α` that is a monoid and also has the ability to distribute the negation operation, and for any natural number `n` which is odd, the power of the negation of any element `a` of the type `α` to the `n` is equal to the negation of `a` to the power `n`. In other words, if `n` is odd, then negating `a` before raising it to the power `n` has the same result as negating the result of raising `a` to the power `n`. This property is often used in number theory and algebra.
More concisely: For any monoid `α` with distributive negation and odd natural number `n`, the negation of `a` to the power `n` equals the power of the negation of `a` to `n`.
|
Even.exists_two_nsmul
theorem Even.exists_two_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] (m : α), Even m → ∃ c, m = 2 • c
The theorem `Even.exists_two_nsmul` states that for any type `α` that is an additive monoid, for any element `m` of `α`, if `m` is even (which means there exists some `r` such that `m = r + r`), then there exists a corresponding element `c` such that `m` is equal to two times `c`. In other words, being "even" in this context means that the element can be expressed as twice some other element.
More concisely: For any additive monoid type `α` and even element `m` of `α`, there exists an element `c` such that `m = 2 * c`.
|
Mathlib.Algebra.Parity._auxLemma.12
theorem Mathlib.Algebra.Parity._auxLemma.12 :
∀ {α : Type u_2} [inst : SubtractionMonoid α] {a : α}, Even (-a) = Even a
This theorem states that for any type `α` that is a subtraction monoid (i.e., a structure with a subtraction operation that obeys certain properties), if an element `a` of `α` is even (meaning it can be expressed as the sum of two equal values), then the negation of `a` is also even. Conversely, if the negation of `a` is even, then `a` itself is also even. The "evenness" of a number is preserved under negation.
More concisely: For any subtraction monoid type `α`, if `a` is an even element, then the negation of `a` is even, and vice versa.
|
Mathlib.Algebra.Parity._auxLemma.20
theorem Mathlib.Algebra.Parity._auxLemma.20 :
∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → ∀ (b : α), Even (a * b) = True
This theorem states that for any type `α` that is a semiring, if an element `m` of `α` is even, then for any other element `n` of `α`, the product `m * n` is also even. In the mathematical terms, if `m` is an even number in the ring, meaning there exists another number `r` in the ring such that `m = r + r`, then for any number `n` in the ring, the statement that `m * n` is also an even number is always true.
More concisely: If `α` is a semiring and `m` is an even element of `α`, then `m * n` is even for all `n` in `α`.
|
Even.pow_nonneg
theorem Even.pow_nonneg :
∀ {R : Type u_4} [inst : LinearOrderedSemiring R] [inst_1 : ExistsAddOfLE R] {n : ℕ},
Even n → ∀ (a : R), 0 ≤ a ^ n
The theorem `Even.pow_nonneg` states that for any type `R`, which is a linear ordered ring, and for any natural number `n` which is even, the nth power of any element `a` from the type `R` is non-negative, i.e., greater than or equal to zero. In other words, if `n` is an even number, then the nth power of any element in a linear ordered ring is always non-negative.
More concisely: For every linear ordered ring R and every even natural number n, the nth power of any element a in R is non-negative (i.e., ≥ 0).
|
Mathlib.Algebra.Parity._auxLemma.8
theorem Mathlib.Algebra.Parity._auxLemma.8 : ∀ {α : Type u_2} [inst : AddZeroClass α], Even 0 = True
The theorem `Mathlib.Algebra.Parity._auxLemma.8` asserts that for any type `α` which has an addition operation with a zero element (`AddZeroClass α`), the number zero (`0`) is considered to be an even number. This is based on the definition of evenness in this context, which specifies that a number is even if it can be expressed as the sum of two identical numbers (say `r + r`). Here, `0` can be seen as `0 + 0`, thus meeting the criterion to be classified as even.
More concisely: The theorem `Mathlib.Algebra.Parity._auxLemma.8` states that in any type `α` with an additive zero, the additive zero `0` is even, i.e., it can be expressed as the sum of two identical elements.
|
Even.neg_pow
theorem Even.neg_pow :
∀ {α : Type u_2} [inst : Monoid α] {n : ℕ} [inst_1 : HasDistribNeg α], Even n → ∀ (a : α), (-a) ^ n = a ^ n := by
sorry
This theorem states that for any type `α` that is a monoid and has the ability to distribute negation, and any natural number `n` that is even, the negative of any element `a` of type `α` raised to the power `n` equals that element `a` raised to the power `n`. In mathematical terms, if `n` is even, then `(-a)^n = a^n` for any `a` in `α`.
More concisely: For any monoid `α` with distributive negation and even natural number `n`, (-`a`)^`n` = `a`^`n` for all `a` in `α`.
|
even_iff_two_dvd
theorem even_iff_two_dvd : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a ↔ 2 ∣ a
This theorem states that for any element `a` of a type `α` that forms a semiring, `a` is even if and only if `a` is divisible by 2. In more mathematical terms, let `α` be a semiring. For any `a` in `α`, `a` satisfies the property `Even` (i.e., there exists some `r` in `α` such that `a = r + r`) if and only if `2` divides `a` (i.e., there exists some `k` in `α` such that `a = 2 * k`).
More concisely: In a semiring, an element is even if and only if it is divisible by 2.
|
Odd.pos
theorem Odd.pos :
∀ {α : Type u_2} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Nontrivial α] {a : α}, Odd a → 0 < a := by
sorry
This theorem states that for any type `α` that is a `CanonicallyOrderedCommSemiring` and is nontrivial, if a number `n` of type `α` is odd, then `n` is strictly greater than 0. In other words, all odd numbers in such a semiring are positive.
More concisely: For any nontrivial `CanonicallyOrderedCommSemiring` type `α`, all odd elements `n` of `α` are strictly positive (i.e., `0 < n`).
|
Odd.exists_bit1
theorem Odd.exists_bit1 : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd a → ∃ b, a = bit1 b
The theorem `Odd.exists_bit1` states that for any type `α` which is a semiring, if an element `a` of `α` is odd, then there exists another element `b` such that `a` can be expressed as `bit1 b`. Here, `bit1 b` adds one to twice `b`. Essentially, the theorem provides an alternate way of expressing an odd number in a semiring; instead of saying it's of the form `2*k + 1`, we can say it's of the form `bit1 b`.
More concisely: For any semiring `α` and odd element `a` in `α`, there exists an element `b` such that `a = bit1 b`.
|
even_bit0
theorem even_bit0 : ∀ {α : Type u_2} [inst : Semiring α] (a : α), Even (bit0 a)
The theorem `even_bit0` states that for all elements `a` of any type `α` that forms a semiring, the function `bit0 a` (which returns `a + a`) produces an "Even" number. Here, an element is considered "Even" if it can be expressed as the sum of two identical elements. Thus, the result `a + a` by definition is always an Even number.
More concisely: For all semiring elements `a`, the result of adding `a` to itself, `a + a`, is an element expressible as the sum of two identical elements. In other words, `a + a` is even.
|
Even.two_dvd
theorem Even.two_dvd : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → 2 ∣ a
The theorem `Even.two_dvd` states that for any type `α` equipped with a semiring structure, if an element `a` of `α` is even (meaning there exists another element `r` such that `a = r + r`), then `2` divides `a`. Here, `2 ∣ a` signifies that `a` can be expressed as `2 * d` for some `d` in `α`.
More concisely: For any semiring `α` and even element `a` in `α`, there exists an element `d` in `α` such that `a = 2 * d`. Therefore, `2` divides `a`.
|
isSquare_of_exists_sq
theorem isSquare_of_exists_sq : ∀ {α : Type u_2} [inst : Monoid α] (m : α), (∃ c, m = c ^ 2) → IsSquare m
This theorem, referred to as `isSquare_of_exists_sq`, states that for any type `α` equipped with a multiplication operation (that forms a Monoid), if there exists an element `c` such that a given element `m` is equal to the square of `c` (expressed as `m = c ^ 2`), then `m` is a square. In simpler terms, if you can find some `c` such that `m` is `c` squared, then `m` satisfies the property of being a square. This is essentially an alternate formulation of the definition of a square in this context.
More concisely: If `m` is the square of some element `c` in a monoid `α` with multiplication operation, then `m` is a square.
|
even_op_iff
theorem even_op_iff : ∀ {α : Type u_2} [inst : Add α] {a : α}, Even (AddOpposite.op a) ↔ Even a
This theorem, `even_op_iff`, states that for any type `α` which supports addition (denoted by `[inst : Add α]`), and any element `a` of that type, `a` is even if and only if its additive opposite (given by `AddOpposite.op a`) is even. In other words, an element and its additive opposite have the same "evenness". Here, "evenness" is defined in terms of additive doubling: an element `a` is even if there exists some `r` such that `a = r + r`.
More concisely: For any type `α` with additation and for all `a` in `α`, `a` is even if and only if its additive inverse is even, where evenness is defined as having a representation as a sum of two equals.
|
IsSquare.inv
theorem IsSquare.inv : ∀ {α : Type u_2} [inst : DivisionMonoid α] {a : α}, IsSquare a → IsSquare a⁻¹
The theorem `IsSquare.inv` states that for any type `α` that is a Division Monoid, if an element `a` of `α` is a square (meaning there exists some `r` in `α` such that `a = r * r`), then the multiplicative inverse of `a`, denoted `a⁻¹`, is also a square. This is essentially saying that the property of being a square is preserved under taking multiplicative inverses in a Division Monoid.
More concisely: If `α` is a Division Monoid and `a` is a square in `α` (i.e., there exists `r` in `α` such that `a = r * r`), then `a⁻¹` is also a square.
|
IsSquare.map
theorem IsSquare.map :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β]
[inst_2 : FunLike F α β] [inst_3 : MonoidHomClass F α β] {m : α} (f : F), IsSquare m → IsSquare (f m)
This theorem, `IsSquare.map`, states that for any types `F`, `α`, and `β` where `α` and `β` are both `MulOneClass` (types with multiplication and a multiplicative identity), and `F` is a function-like structure from `α` to `β` and a monoid homomorphism, if an element `m` of type `α` is a square (that is, there exists an `r` such that `m = r * r`), then the image of this element under the function `f` of type `F` is also a square in `β`. In simple terms, it says that the image of a square under a monoid homomorphism is also a square.
More concisely: If `f` is a monoid homomorphism from a type `α` (with multiplicative identity) to a type `β` (also with multiplicative identity), and `m` is a square in `α`, then `f(m)` is a square in `β`.
|
Mathlib.Algebra.Parity._auxLemma.18
theorem Mathlib.Algebra.Parity._auxLemma.18 : ∀ {α : Type u_2} [inst : Semiring α], Even 2 = True
The theorem `Mathlib.Algebra.Parity._auxLemma.18` asserts that for any type `α` equipped with a semiring structure, the number `2` is Even. In more mathematical terms, it states that there exists some element `r` in the semiring `α` such that `2` is equal to `r + r`.
More concisely: For any semiring `α`, there exists an element `r` in `α` such that `2 = r + r`.
|
Even.neg_one_pow
theorem Even.neg_one_pow :
∀ {α : Type u_2} [inst : Monoid α] {n : ℕ} [inst_1 : HasDistribNeg α], Even n → (-1) ^ n = 1
The theorem `Even.neg_one_pow` states that for any natural number `n` in a monoidal type `α` that also has a notion of negation, if `n` is even (i.e., there exists an `r` in `α` such that `n = r + r`), then the power of `-1` raised to `n` is `1`. In mathematical terms, this can be written as if $n$ is even, then $(-1)^n = 1$.
More concisely: For any even natural number `n` in a monoidal type `α` with negation, (-1)^n = 1.
|
Even.add_odd
theorem Even.add_odd : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Even a → Odd b → Odd (a + b)
The theorem `Even.add_odd` states that for any type `α` that is a semiring, if we have two elements `m` and `n` of this type, with `m` being even and `n` being odd, then the sum of `m` and `n` is also odd. In mathematical terms, if there exists some `r` such that `m = r + r` (definition of `m` being even) and there exists some `k` such that `n = 2*k + 1` (definition of `n` being odd), then there exists some `l` such that `m + n = 2*l + 1`, which makes `m + n` odd.
More concisely: If `m` is even and `n` is odd in a semiring, then their sum `m + n` is odd. ( mathematically expressed as: `∃ r, m = r + r ∧ ∃ k, n = 2*k + 1 → ∃ l, m + n = 2*l + 1`)
|
Mathlib.Algebra.Parity._auxLemma.2
theorem Mathlib.Algebra.Parity._auxLemma.2 : ∀ {α : Type u_2} [inst : Add α] (m : α), Even (m + m) = True
This theorem states that for any type `α` that supports addition, and for any element `m` of type `α`, the statement "`m + m` is Even" is always true. Here, an element `a` of a type `α` is said to be Even if it can be expressed as `r + r` for some `r` of type `α`.
More concisely: For any type `α` with additive structure and any `α` element `m`, `m + m` is an even element.
|