sq_sub_sq
theorem sq_sub_sq : ∀ {R : Type u_1} [inst : CommRing R] (a b : R), a ^ 2 - b ^ 2 = (a + b) * (a - b)
This theorem, `sq_sub_sq`, states that for any commutative ring `R` and any two elements `a` and `b` of `R`, the square of `a` minus the square of `b` equals the product of `a + b` and `a - b`. This is a generalization of the familiar algebraic identity $(a^2 - b^2) = (a + b)(a - b)$ to the context of commutative rings.
More concisely: For any commutative ring R and elements a, b ∈ R, a^2 - b^2 = (a + b) * (a - b).
|
neg_pow
theorem neg_pow :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ n = (-1) ^ n * a ^ n := by
sorry
This theorem, `neg_pow`, states that for any type `R` that is a monoid and has the ability to distribute over negation (i.e., has an operation `-` that distributes over `*`), and for any element `a` of type `R` and any natural number `n`, the `n`th power of `-a` is equal to the `n`th power of `-1` multiplied by the `n`th power of `a`. In mathematical notation, this would be expressed as `(-a)^n = (-1)^n * a^n`.
More concisely: For any monoid `R` with distributive negation and for all `a` in `R` and natural number `n`, `(-a)^n = (-1)^n * a^n`.
|
neg_pow_two
theorem neg_pow_two : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R), (-a) ^ 2 = a ^ 2 := by
sorry
This theorem, referred to as `neg_pow_two`, states that for any type `R` that is a monoid and supports negation, the square of the negation of an element `a` from `R` is equal to the square of `a` itself. In mathematical terms, it can be expressed as $(-a)^2 = a^2$ for any element `a` in `R`.
More concisely: For any monoid `R` with negation, $-(-a) = a$. Equivalently, $(-a)^2 = a^2$.
|
pow_two_sub_pow_two
theorem pow_two_sub_pow_two : ∀ {R : Type u_1} [inst : CommRing R] (a b : R), a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
sorry
This theorem, named `pow_two_sub_pow_two`, states that for any commutative ring `R` and any two elements `a` and `b` of `R`, the difference of the squares of `a` and `b` is equal to the product of the sum and difference of `a` and `b`. In mathematical notation, it's expressing the identity $a^2 - b^2 = (a+b)(a-b)$.
More concisely: For any commutative ring R and its elements a and b, the difference of their squares equals the product of their sum and difference: a^2 - b^2 = (a + b)(a - b).
|
neg_one_sq
theorem neg_one_sq : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R], (-1) ^ 2 = 1
This theorem states that in any monoid R, which additionally has the property of distributing negations (i.e., it respects the distributive law for negation), the square of -1 is equal to 1. In mathematical terms, this can be written as (-1)^2 = 1. This theorem holds under the specific conditions that R is a monoid and respects the distributive law for negation.
More concisely: In a monoid R with distributive negations, (-1)^2 equals 1.
|
neg_one_pow_eq_pow_mod_two
theorem neg_one_pow_eq_pow_mod_two : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ), (-1) ^ n = (-1) ^ (n % 2)
This theorem states that for any natural number `n` in any ring `R`, the power of -1 raised to `n` is equal to the power of -1 raised to the modulus of `n` by 2. In simpler terms, the value of -1 to the power of any number is the same as -1 to the power of that number mod 2. This is because -1 to the power of any even number is 1, and -1 to the power of any odd number is -1.
More concisely: For any natural number n in a ring R, (-1)^n = (-1)^(n % 2).
|
neg_one_pow_eq_or
theorem neg_one_pow_eq_or :
∀ (R : Type u_1) [inst : Monoid R] [inst_1 : HasDistribNeg R] (n : ℕ), (-1) ^ n = 1 ∨ (-1) ^ n = -1
This theorem, `neg_one_pow_eq_or`, states that for any type `R` that is a monoid and has a distributive negation, and for any natural number `n`, the value of `(-1) ^ n` is either `1` or `-1`. In mathematical terms, it asserts that the power of `-1` for any non-negative integer will always be `1` or `-1`.
More concisely: For any monoid `R` with distributive negation, the value of `(-1) ^ n` is equal to `1` or `-1` for every natural number `n`.
|
neg_one_pow_two
theorem neg_one_pow_two : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R], (-1) ^ 2 = 1
This theorem, named `neg_one_pow_two`, states that in any monoid `R` that also supports negation operation, the square of `-1` is equal to `1`. In other words, for all types `R` where `R` is a monoid and has a distributive negation operation, the expression `(-1)^2` is always equal to `1`.
More concisely: In any monoid with a distributive negation operation, (-1)^2 equals 1.
|
sub_pow_two
theorem sub_pow_two : ∀ {R : Type u_1} [inst : CommRing R] (a b : R), (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
sorry
The theorem `sub_pow_two` states that for any commutative ring `R` and any two elements `a` and `b` of `R`, the square of the difference `(a - b)^2` equals `a^2 - 2ab + b^2`. This is a standard result in algebra, often called the square of a binomial, and it gives a specific form for expanding the square of a subtraction.
More concisely: For any commutative ring R and elements a, b ∈ R, (a - b)^2 = a^2 - 2ab + b^2.
|
RingHom.map_pow
theorem RingHom.map_pow :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (a : R) (n : ℕ),
f (a ^ n) = f a ^ n
This theorem states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, any element `a` of `R`, and any non-negative integer `n`, the image of `a` to the power of `n` under `f` is the same as the image of `a` under `f` to the power of `n`. In other words, the ring homomorphism preserves the power operation.
More concisely: For any semirings R and S, any ring homomorphism f : R -> S, and any element a of R and non-negative integer n, f (a^n) = (f(a))^n.
|
sq_eq_one_iff
theorem sq_eq_one_iff :
∀ {R : Type u_1} [inst : Ring R] {a : R} [inst_1 : NoZeroDivisors R], a ^ 2 = 1 ↔ a = 1 ∨ a = -1
This theorem states that for any element 'a' in a ring 'R' that does not contain zero divisors (NoZeroDivisors R), the square of 'a' is equal to 1 if and only if 'a' is either 1 or -1. Here, '^' is the exponentiation operation, and '∨' represents the logical OR operation. This means that if 'a' squared is 1, then 'a' must be 1 or -1, and if 'a' is either 1 or -1, its square will be 1.
More concisely: For any element 'a' in a ring without zero divisors, 'a'^2 = 1 if and only if 'a' = 1 or 'a' = -1.
|
add_pow_two
theorem add_pow_two : ∀ {R : Type u_1} [inst : CommSemiring R] (a b : R), (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
sorry
The theorem `add_pow_two` is an alias of `add_sq`. It states that for any type `R` that is a commutative semiring, and for any elements `a` and `b` of `R`, the square of the sum `(a + b) ^ 2` is equal to the sum of the square of `a`, twice the product of `a` and `b`, and the square of `b`, expressed as `a ^ 2 + 2 * a * b + b ^ 2`. This is essentially a formal version of the well-known algebraic identity $(a + b)^2 = a^2 + 2ab + b^2$.
More concisely: For any commutative semiring `R` and elements `a` and `b` in `R`, `(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2`.
|
neg_pow_bit1
theorem neg_pow_bit1 :
∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ bit1 n = -a ^ bit1 n := by
sorry
This theorem states that for any type `R` which is a `Monoid` and also supports negation (`HasDistribNeg`), for any element `a` of type `R` and any natural number `n`, the negative of `a` raised to the power of `2n + 1` (denoted by `bit1 n`) is equal to the negation of `a` raised to the power of `2n + 1`. In mathematical terms, given any `a` in `R` and any natural number `n`, we have `(-a)^(2n + 1) = -(a^(2n + 1))`.
More concisely: For any monoid `R` with negation (`HasDistribNeg`), and for all `a` in `R` and natural number `n`, `(-a)^(2n + 1) = -(a^(2n + 1))`.
|
neg_sq
theorem neg_sq : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R), (-a) ^ 2 = a ^ 2
This theorem, `neg_sq`, states that for any type `R` that is a monoid and supports distributed negation, the square of the negation of any element `a` from `R`, is equal to the square of `a` itself. In mathematical terms, this theorem says that `(-a)^2 = a^2` for all `a` in `R`. This is a generalization of a common property in number systems, that the square of a number and its negation are equal.
More concisely: For any monoid `R` with distributed negation, `(-a)^2 = a^2` for all `a` in `R`.
|
add_sq
theorem add_sq : ∀ {R : Type u_1} [inst : CommSemiring R] (a b : R), (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
This theorem, named `add_sq`, states that for any commutative semiring `R` and for any elements `a` and `b` in `R`, the square of the sum of `a` and `b` is equal to the sum of the square of `a`, twice the product of `a` and `b`, and the square of `b`. In mathematical notation, this is expressed as `(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2`. This is a classic result in algebra known as the square of a binomial.
More concisely: For any commutative semiring `R` and elements `a` and `b` in `R`, `(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2`.
|