CharP.cast_card_eq_zero
theorem CharP.cast_card_eq_zero :
∀ (R : Type u_1) [inst : AddGroupWithOne R] [inst_1 : Fintype R], ↑(Fintype.card R) = 0
The theorem `CharP.cast_card_eq_zero` states that for any type `R` that has both an `AddGroupWithOne` and a `Fintype` instance, the cardinality of `R` (the number of elements in `R`), when cast to `R`, is equal to zero. In mathematical terms, this means that the size of the set `R` is equal to the characteristic of the additive group with one on `R`.
More concisely: The cardinality of an additive group with one on a type `R` having both `AddGroupWithOne` and `Fintype` instances equals zero.
|
Ring.neg_one_ne_one_of_char_ne_two
theorem Ring.neg_one_ne_one_of_char_ne_two :
∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : Nontrivial R], ringChar R ≠ 2 → -1 ≠ 1
The theorem `Ring.neg_one_ne_one_of_char_ne_two` states that for any type `R` which has a structure of a non-associative ring and is nontrivial (i.e., it has at least two distinct elements), if the characteristic of the ring is not equal to 2, then -1 is not equal to 1 in that ring. The characteristic of a ring is a fundamental property in number theory and algebra, and refers to the smallest positive integer `n` such that `n * x = 0` for every element `x` in the ring, or zero if no such integer exists.
More concisely: For any non-associative ring R with at least two distinct elements and characteristic different from 2, -1 is not equal to 1.
|
sub_pow_char_of_commute
theorem sub_pow_char_of_commute :
∀ (R : Type u_1) [inst : Ring R] {p : ℕ} [inst_1 : Fact p.Prime] [inst_2 : CharP R p] (x y : R),
Commute x y → (x - y) ^ p = x ^ p - y ^ p
The theorem `sub_pow_char_of_commute` states that for any given ring `R` and natural number `p` that is prime, and for any two elements `x` and `y` of the ring `R` that commute (i.e., `x * y = y * x`), the p-th power of the difference of `x` and `y` (i.e., `(x - y) ^ p`) is equal to the difference of the p-th power of `x` and `y` (i.e., `x ^ p - y ^ p`). This theorem makes use of the characteristic of the ring being equal to the prime number `p` (denoted by `CharP R p` in Lean).
More concisely: For any commuting elements x and y in a ring of prime characteristic p, (x - y)^p = x^p - y^p.
|
ringChar.spec
theorem ringChar.spec : ∀ (R : Type u_1) [inst : NonAssocSemiring R] (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
The theorem `ringChar.spec` states that for any type `R` which is a non-associative semiring (denoted by `[inst : NonAssocSemiring R]`) and any natural number `x`, `x` (when promoted to the type `R`) is equal to zero if and only if `x` is divisible by the unique characteristic (`ringChar R`) of the semiring `R`.
More concisely: For any non-associative semiring R and natural number x, x = 0 in R if and only if x is congruent to 0 modulo the unique characteristic of R.
|
CharP.ringChar_ne_one
theorem CharP.ringChar_ne_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : Nontrivial R], ringChar R ≠ 1
The theorem `CharP.ringChar_ne_one` asserts that for any type `R`, if `R` has a non-associative semiring structure and `R` is nontrivial (i.e., there exist two distinct elements in `R`), then the unique characteristic of the semiring `R` (denoted as `ringChar R`) is not equal to 1. This means that in a nontrivial, non-associative semiring, the unique characteristic cannot be 1.
More concisely: In a nontrivial, non-associative semiring, the unique characteristic is not equal to 1.
|
Ring.eq_self_iff_eq_zero_of_char_ne_two
theorem Ring.eq_self_iff_eq_zero_of_char_ne_two :
∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : Nontrivial R] [inst_2 : NoZeroDivisors R],
ringChar R ≠ 2 → ∀ {a : R}, -a = a ↔ a = 0
This theorem states that for any non-associative ring `R`, which has no zero divisors and is non-trivial (i.e., it has at least two distinct elements), if the unique characteristic of the ring `R` is not equal to `2`, then for any element `a` in `R`, `-a` is equal to `a` if and only if `a` is equal to zero.
More concisely: In a non-associative ring `R` with no zero divisors and characteristic different from 2, the additive inverse of an element `a` equals `a` if and only if `a` is the additive identity.
|
CharP.cast_eq_zero_iff
theorem CharP.cast_eq_zero_iff :
∀ (R : Type u) [inst : AddMonoidWithOne R] (p : ℕ) [inst_1 : CharP R p] (x : ℕ), ↑x = 0 ↔ p ∣ x
This theorem states that for any type `R` that is equipped with the structure of an additive monoid with unit and has characteristic `p`, and for any natural number `x`, the cast of `x` to `R` is equal to zero if and only if `p` divides `x`. This theorem provides a way to check divisibility by `p` using the properties of the characteristic of the ring `R`.
More concisely: For any additive monoid with unit and characteristic `p` type `R`, the element `x` in `R` obtained by casting a natural number `x` is equal to zero if and only if `p` divides `x`.
|
CharP.cast_eq_zero
theorem CharP.cast_eq_zero : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [inst_1 : CharP R p], ↑p = 0 := by
sorry
This theorem states that for any type `R` that has an instance of `AddMonoidWithOne` (meaning it is a mathematical object with an operation similar to addition and a "one" element), and a natural number `p` that has a characteristic `CharP` associated with `R`, the cast of `p` to `R` equals zero. In mathematical terms, this theorem states that in a ring `R` of characteristic `p`, the element `p` of the ring is the additive identity, i.e., it behaves like the number zero.
More concisely: In a ring of characteristic `p`, the element `p` behaves as the additive identity.
|
ringChar.eq
theorem ringChar.eq : ∀ (R : Type u_1) [inst : NonAssocSemiring R] (p : ℕ) [C : CharP R p], ringChar R = p
This theorem states that for any type `R` that forms a non-associative semiring, and any natural number `p` for which `R` has characteristic `p`, the unique characteristic of the semiring `R` (as computed by the `ringChar` function) is equal to `p`. Essentially, this means that the `ringChar` function correctly computes the characteristic of a semiring.
More concisely: For any non-associative semiring `R` of characteristic `p`, the `ringChar` function returns `p`.
|
CharP.eq
theorem CharP.eq : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] {p q : ℕ}, CharP R p → CharP R q → p = q
This theorem states that for any type `R` which has an `AddMonoidWithOne` structure, if `R` has characteristic `p` and `R` has characteristic `q`, then `p` must be equal to `q`. In the context of ring theory, the characteristic of a ring is the smallest positive number of times you have to add the ring's multiplicative identity to itself to get the additive identity, or zero if this number doesn't exist. This theorem guarantees that this characteristic is unique, so if `p` and `q` are both characteristics of the same ring, they must be equal.
More concisely: If a type `R` with an `AddMonoidWithOne` structure has two distinct characteristics `p` and `q`, then `p` is not the characteristic of `R`. Therefore, the characteristic of `R` is unique and must be equal to any given characteristic `p` or `q`.
|
add_pow_char_of_commute
theorem add_pow_char_of_commute :
∀ (R : Type u_1) [inst : Semiring R] {p : ℕ} [hp : Fact p.Prime] [inst_1 : CharP R p] (x y : R),
Commute x y → (x + y) ^ p = x ^ p + y ^ p
The theorem `add_pow_char_of_commute` states that, for any type `R` which is a semiring, and for any natural number `p` which is prime (characteristic of `R` is `p`), given any two elements `x` and `y` of `R` that commute, that is `x * y = y * x`, the power of the sum `(x + y)` to the `p` equals the sum of the power `x` to the `p` and `y` to the `p`. In mathematical terms, it can be stated as: if `x` and `y` commute in a semiring `R` and `p` is a prime number that is also the characteristic of `R`, then `(x + y)^p = x^p + y^p`.
More concisely: If `x` and `y` commute in a semiring `R` of prime characteristic `p`, then `(x + y)^p = x^p + y^p`.
|
ringChar.dvd
theorem ringChar.dvd : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {x : ℕ}, ↑x = 0 → ringChar R ∣ x
The theorem `ringChar.dvd` states that for any type `R` which is a `NonAssocSemiring` and any natural number `x`, if the natural number `x` cast to `R` is zero, then the characteristic of the semiring `R`, denoted as `ringChar R`, divides `x`. In other words, if `x` becomes zero when considered as an element of `R`, then `x` is a multiple of the unique characteristic of the semiring `R`.
More concisely: If a natural number `x` maps to zero in a non-associative semiring `R`, then the characteristic of `R` divides `x`.
|
CharP.char_ne_one
theorem CharP.char_ne_one :
∀ (R : Type u_1) [inst : NonAssocSemiring R] [inst_1 : Nontrivial R] (p : ℕ) [hc : CharP R p], p ≠ 1
This theorem states that for any type `R` that has a structure of a non-associative semiring and is nontrivial, if `R` has characteristic `p` (which is a natural number), then `p` cannot be equal to 1. In mathematical terms, a ring has characteristic `p` if every element of the ring, when added to itself `p` times, results in the zero element of the ring. Nontrivial means that there exists at least two distinct elements in the ring, and a non-associative semiring is a semiring where the multiplication is not necessarily associative.
More concisely: A nontrivial non-associative semiring `R` with characteristic `1` is the empty set.
|
Commute.add_pow_prime_pow_eq
theorem Commute.add_pow_prime_pow_eq :
∀ {R : Type u_1} [inst : Semiring R] {p : ℕ} {x y : R},
p.Prime →
Commute x y →
∀ (n : ℕ),
(x + y) ^ p ^ n =
x ^ p ^ n + y ^ p ^ n +
↑p * (Finset.Ioo 0 (p ^ n)).sum fun k => x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
This theorem states that for any semiring `R`, prime number `p`, and elements `x` and `y` from `R` that commute, for any natural number `n`, the power of the sum of `x` and `y` raised to the power `p ^ n` is equal to the sum of `x ^ p ^ n`, `y ^ p ^ n`, and the product of `p` and the sum over all `k` in the interval `(0, p ^ n)` of the product of `x ^ k`, `y ^ (p ^ n - k)`, and the binomial coefficient `Nat.choose (p ^ n) k` divided by `p`. In mathematical notation, this can be written as $(x + y)^{p^n} = x^{p^n} + y^{p^n} + p\sum_{k=0}^{p^n} x^k * y^{p^n - k} * \binom{p^n}{k}/p$.
More concisely: For any semiring `R`, prime number `p`, and commuting elements `x`, `y` from `R`, $(x + y)^{p^n} = x^{p^n} + y^{p^n} + p\sum\_{k=0}^{p^n} \binom{p^n}{k}x^k y^{p^n-k}$.
|
ringChar.eq_iff
theorem ringChar.eq_iff : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ}, ringChar R = p ↔ CharP R p
This theorem states that for any type `R` which has the structure of a `NonAssocSemiring`, and for any natural number `p`, the unique characteristic of the semiring `R` is equal to `p` if and only if `R` has characteristic `p`. In other words, the ring characteristic function `ringChar R` equals `p` if and only if `CharP R p` holds, where `CharP R p` is a predicate that asserts `R` has characteristic `p`. This establishes a direct correspondence between the property of a semiring having a certain characteristic and the value of the `ringChar` function.
More concisely: For any semiring R with characteristic p as a NonAssocSemiring, the unique characteristic of R equals p if and only if the predicate CharP (R p) holds.
|
add_pow_char_pow_of_commute
theorem add_pow_char_pow_of_commute :
∀ (R : Type u_1) [inst : Semiring R] {p n : ℕ} [hp : Fact p.Prime] [inst_1 : CharP R p] (x y : R),
Commute x y → (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
The theorem `add_pow_char_pow_of_commute` states that for any semiring `R` of characteristic `p`, where `p` is a prime number, and for any elements `x` and `y` of `R` that commute with each other (i.e., `x * y = y * x`), the power of the sum of `x` and `y` to the power of `p` raised to `n` is equal to the sum of the powers of `x` and `y` each to the power of `p` raised to `n`. In mathematical notation, this can be expressed as `(x + y) ^ p^n = x ^ p^n + y ^ p^n`. This property holds only when `x` and `y` commute, meaning that the order in which they are multiplied does not affect the result.
More concisely: For any semiring of characteristic `p` and commuting elements `x` and `y`, `(x + y) ^ p^n = x ^ p^n + y ^ p^n`.
|
Int.cast_injOn_of_ringChar_ne_two
theorem Int.cast_injOn_of_ringChar_ne_two :
∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : Nontrivial R], ringChar R ≠ 2 → Set.InjOn Int.cast {0, 1, -1}
This theorem states that for any non-associative ring `R` that is nontrivial (i.e., has at least two distinct elements) and has a characteristic not equal to `2`, the canonical homomorphism from the integers to `R` is injective when restricted to the set `{0, 1, -1}`. In other words, if two integers from this set are mapped to the same element in `R`, then they must have been the same integer to begin with.
More concisely: For any non-associative nontrivial ring R of characteristic different from 2, the canonical homomorphism from the integers to R maps {0, 1, -1} injectively.
|
CharP.charP_to_charZero
theorem CharP.charP_to_charZero : ∀ (R : Type u_2) [inst : AddGroupWithOne R] [inst_1 : CharP R 0], CharZero R := by
sorry
This theorem states that for any type `R` that forms an additive group with an identity element, if `R` has characteristic `0`, then `R` also satisfies the property of being `CharZero`. In the field of mathematics, a ring `R` is said to have characteristic `0` if and only if for any positive integer `n`, `n` times the multiplicative identity is not the additive identity. The `CharZero` property indicates that the natural number embedding into `R` is injective. Thus, this theorem provides a link between the characteristic of a ring and an important property about its structure.
More concisely: If `R` is an additive group with an identity element and has characteristic 0, then `R` is a CharZero ring.
|
Ring.two_ne_zero
theorem Ring.two_ne_zero :
∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Nontrivial R], ringChar R ≠ 2 → 2 ≠ 0
This theorem states that, in any nontrivial ring (a ring that has at least two distinct elements) with a non-associated semiring structure (a semiring where the associative law of multiplication may not hold), if the unique characteristic of the ring is not equal to `2`, then `2` is not equal to `0` in that ring. In other words, the number `2` is not identified with the zero element in such a ring whose characteristic is not `2`.
More concisely: In a nontrivial ring with a non-associative semiring structure, if the characteristic is not 2, then 2 ≠ 0.
|
CharP.exists
theorem CharP.exists : ∀ (R : Type u_1) [inst : NonAssocSemiring R], ∃ p, CharP R p
This theorem states that for any type `R` which is a non-associative semiring, there exists a prime number `p` such that `R` has characteristic `p`. In other words, for any non-associative semiring, there exists a prime number `p` such that adding `p` copies of any element of `R` together will always yield the additive identity (zero) of the semiring.
More concisely: For any non-associative semiring R, there exists a prime number p such that the sum of p elements of R is the additive identity.
|
CharP.char_ne_zero_of_finite
theorem CharP.char_ne_zero_of_finite :
∀ (R : Type u_1) [inst : NonAssocRing R] (p : ℕ) [inst : CharP R p] [inst : Finite R], p ≠ 0
This theorem states that the characteristic of a finite non-associative ring cannot be zero. In other words, for any finite non-associative ring R with characteristic p, it ensures that p cannot be zero. Here, a ring's characteristic is defined as the smallest positive integer for which the repeated addition of 1 (n times) gives 0 in the ring; for a finite ring, this characteristic must be a positive integer.
More concisely: A finite non-associative ring has non-zero characteristic.
|
CharP.char_is_prime_or_zero
theorem CharP.char_is_prime_or_zero :
∀ (R : Type u_1) [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : Nontrivial R] (p : ℕ)
[hc : CharP R p], p.Prime ∨ p = 0
The theorem `CharP.char_is_prime_or_zero` states that for any type `R` that has the structure of a non-associative semiring (i.e., a mathematical structure that behaves like numbers under addition and multiplication, but multiplication doesn't necessarily associate) and additionally has no zero divisors and is nontrivial (i.e., `R` contains at least two distinct elements), and for any natural number `p` such that `R` has characteristic `p` (i.e., `p` is the least positive integer such that `p` times any element of `R` is zero), then `p` is either a prime number or zero. Here, a prime number is defined as a natural number greater than or equal to 2 whose only divisors are itself and 1.
More concisely: In a non-associative semiring without zero divisors and of nontrivial size, the characteristic is either 0 or a prime number.
|