expChar_pow_pos
theorem expChar_pow_pos : ∀ (R : Type u) [inst : Semiring R] (q : ℕ) [inst : ExpChar R q] (n : ℕ), 0 < q ^ n
This theorem states that any power of the exponential characteristic is positive. Given a semiring `R` and a natural number `q` which is the exponential characteristic of `R`, for any natural number `n`, the `n`th power of `q` is greater than zero. In mathematical terms, this can be written as $0 < q^n$ for all natural numbers `n`. Please note that this theorem holds true under the condition that `R` is a semiring and `q` is its exponential characteristic.
More concisely: For any semiring `R` and its exponential characteristic `q`, $0 < q^n$ for all natural numbers `n`.
|
ringExpChar.eq
theorem ringExpChar.eq : ∀ (R : Type u) [inst : Semiring R] (q : ℕ) [h : ExpChar R q], ringExpChar R = q
This theorem states that for any type `R` that has a `Semiring` structure, and for any natural number `q` that has an `ExpChar` (exponential characteristic) structure with `R`, the function `ringExpChar` applied to `R` is equal to `q`. In other words, the unique exponential characteristic of a semiring `R`, as produced by the function `ringExpChar`, is exactly `q`.
More concisely: For any semiring `R` and its associated natural number `q` with an `ExpChar` structure, `ringExpChar R = q`.
|
expChar_is_prime_or_one
theorem expChar_is_prime_or_one : ∀ (R : Type u) [inst : Semiring R] (q : ℕ) [hq : ExpChar R q], q.Prime ∨ q = 1 := by
sorry
This theorem states that for any semiring `R` and any natural number `q` that specifies the exponential characteristic of `R`, the value of `q` is either a prime number or equal to one. In other words, in a semiring, the exponential characteristic is always a prime number or one. The exponential characteristic of a semiring is the smallest positive natural number `n` such that `n` times 1 in the semiring equals 0, or if such a number does not exist, the characteristic is defined to be zero.
More concisely: In any semiring, the exponential characteristic is a prime number or equals one.
|
char_prime_of_ne_zero
theorem char_prime_of_ne_zero :
∀ (R : Type u) [inst : Semiring R] [inst_1 : Nontrivial R] [inst_2 : NoZeroDivisors R] {p : ℕ} [hp : CharP R p],
p ≠ 0 → p.Prime
This theorem states that, given a non-trivial semiring `R` with no zero divisors, if `p` is a non-zero characteristic of `R`, then `p` is prime. In other words, if `p` is a non-zero natural number such that every element of `R` is equivalent to a multiple of `p` (i.e., `p` is the characteristic of `R`), then `p` satisfies the properties of a prime number. It is not zero, it is not a unit, and if it divides the product of two numbers, it must divide at least one of them.
More concisely: If `R` is a non-trivial semiring with no zero divisors and characteristic `p` is a non-zero natural number, then `p` is prime.
|
char_zero_of_expChar_one
theorem char_zero_of_expChar_one :
∀ (R : Type u) [inst : Semiring R] [inst_1 : Nontrivial R] (p : ℕ) [hp : CharP R p] [hq : ExpChar R 1], p = 0 := by
sorry
This theorem states that for any semiring `R` of a certain type `u`, that is nontrivial, if the exponential characteristic of `R` is one, then the characteristic of `R`, denoted by `p`, is zero. In other words, if the exponential function exhibits a particular property (being characterized by one), then the ring `R` must have a certain other property (having characteristic zero).
More concisely: If `R` is a nontrivial semiring of type `u` with exponential characteristic equal to one, then its characteristic `p` is zero.
|
charZero_of_expChar_one'
theorem charZero_of_expChar_one' :
∀ (R : Type u) [inst : Semiring R] [inst_1 : Nontrivial R] [hq : ExpChar R 1], CharZero R
This theorem states that for any type `R` that has the structure of a semiring and is nontrivial (i.e., has at least two distinct elements), if `R` has an exponential characteristic of one, then `R` has a characteristic of zero. An exponential characteristic of one means that every positive integer `n` can be expressed as a power of one in `R`. A characteristic of zero means that `R` contains an isomorphic copy of the integers.
More concisely: If `R` is a nontrivial semiring with exponentially closing identity (every positive integer can be written as a power of 1), then `R` has characteristic zero.
|
ExpChar.exists
theorem ExpChar.exists : ∀ (R : Type u) [inst : Ring R] [inst_1 : IsDomain R], ∃ q, ExpChar R q
This theorem states that for any type `R` which has a ring structure and is a domain, there exists an exponential characteristic `q` of `R`. Here, `q` is a positive natural number (`ℕ+`) or zero (`0`), representing the characteristic of the exponential function in the ring `R`.
More concisely: For any commutative ring `R` that is a domain, there exists a positive natural number or zero denoted as the exponential characteristic `q` of `R`, such that the exponential function `exp : R → R^R` satisfies `exp(x) = ∑ i = 0^∞ (x^i / i!) = 1 + x + x^2 / 2! + ...` with characteristic `q`.
|
char_eq_expChar_iff
theorem char_eq_expChar_iff :
∀ (R : Type u) [inst : Semiring R] (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q], p = q ↔ p.Prime
This theorem states that in a semiring `R`, the characteristic of `R`, denoted as `p`, equals the exponential characteristic, denoted as `q`, if and only if `p` is a prime number. In mathematical terms, for all semirings `R`, and for all natural numbers `p` and `q` where `p` is the characteristic of `R` and `q` is the exponential characteristic of `R`, `p` equals `q` if and only if `p` is prime. A number `p` is prime in the context of a commutative monoid with zero (such as a ring) if it is not zero, not a unit, and if for all elements `a` and `b` of the monoid, if `p` divides the product of `a` and `b`, then `p` divides `a` or `p` divides `b`.
More concisely: In a semiring, the characteristic equals the exponential characteristic if and only if the characteristic is a prime number.
|
expChar_of_injective_ringHom
theorem expChar_of_injective_ringHom :
∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : Semiring A] {f : R →+* A},
Function.Injective ⇑f → ∀ (q : ℕ) [hR : ExpChar R q], ExpChar A q
The theorem `expChar_of_injective_ringHom` states that for any semiring `R` and any semiring `A`, given an injective ring homomorphism `f` from `R` to `A`, if `R` has an exponential characteristic `q`, then `A` will also have the same exponential characteristic `q`. Here, a ring homomorphism `f` is said to be injective if it satisfies the property that whenever `f(x) = f(y)`, it implies that `x = y`. The exponential characteristic of a semiring is a natural number (possibly zero) which characterizes the behavior of exponentiation in the ring.
More concisely: If `f` is an injective ring homomorphism from the semiring `R` with exponential characteristic `q` to the semiring `A`, then `A` also has exponential characteristic `q`.
|
expChar_of_injective_algebraMap
theorem expChar_of_injective_algebraMap :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Function.Injective ⇑(algebraMap R A) → ∀ (q : ℕ) [inst : ExpChar R q], ExpChar A q
The theorem `expChar_of_injective_algebraMap` states that if the algebra map from a commutative semiring `R` to a semiring `A`, given by the `Algebra` structure, is an injective function, then `A` and `R` share the same exponential characteristic. Here, the exponential characteristic of a semiring is a natural number `q` which is either 1 or a prime that divides every `(p^n) - p` for `p` being an element of the semiring and `n` greater than `q`. The theorem refers to the situation when `ExpChar R q` holds, which means `R` has exponential characteristic `q`, and concludes that `A` also has exponential characteristic `q`, denoted as `ExpChar A q`.
More concisely: If the algebra map from a commutative semiring R to a semiring A, given by the Algebra structure, is an injective function and R has exponential characteristic q, then A also has exponential characteristic q.
|
expChar_one_iff_char_zero
theorem expChar_one_iff_char_zero :
∀ (R : Type u) [inst : Semiring R] [inst_1 : Nontrivial R] (p q : ℕ) [inst_2 : CharP R p] [inst : ExpChar R q],
q = 1 ↔ p = 0
This theorem states that in a nontrivial semiring `R`, the exponential characteristic `q` is equal to one if and only if the characteristic `p` of `R` is zero. The characteristic of a ring is the smallest positive integer `n` such that `n` times any element of the ring equals zero. The exponential characteristic of a ring is the smallest positive integer `n` such that `n` to the power any element of the ring equals one.
More concisely: In a semiring R, the exponential characteristic is equal to 1 if and only if the characteristic is zero.
|
ExpChar.eq
theorem ExpChar.eq : ∀ {R : Type u} [inst : Semiring R] {p q : ℕ}, ExpChar R p → ExpChar R q → p = q
This theorem states that for any given semiring `R`, the exponential characteristic is unique. In other words, if both `p` and `q` are exponential characteristics of the semiring `R`, then `p` and `q` must be equal. This is important because it ensures the consistency of the exponential characteristic within a given algebraic structure.
More concisely: In any semiring, the exponential characteristic is unique.
|
expChar_pos
theorem expChar_pos : ∀ (R : Type u) [inst : Semiring R] (q : ℕ) [inst : ExpChar R q], 0 < q
This theorem states that the exponential characteristic of a semiring, R, is always positive. In the context of this theorem, the exponential characteristic of a semiring, represented by the natural number, q, is a property that characterizes how exponentiation behaves in that semiring. Therefore, the theorem asserts that for any semiring R and any exponential characteristic q of R, the value of q will always be greater than zero.
More concisely: The exponential characteristic of any semiring is a positive natural number.
|
expChar_one_of_char_zero
theorem expChar_one_of_char_zero :
∀ (R : Type u) [inst : Semiring R] (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q], q = 1
This theorem states that for any type `R` that has a semiring structure, if the characteristic of `R` is zero and `q` is the exponential characteristic of `R`, then `q` must be equal to 1. In other words, if a semiring has characteristic zero, its exponential characteristic is necessarily one.
More concisely: For any semiring `R` with characteristic zero, its exponential characteristic equals 1.
|
frobenius_def
theorem frobenius_def :
∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (x : R), (frobenius R p) x = x ^ p
The theorem `frobenius_def` states that for any type `R` which is an instance of a commutative semiring, any natural number `p`, and any `x` of type `R`, the application of the Frobenius map (which sends `x` to `x` raised to the power `p`) on `x` is equal to `x` raised to the power `p`. In the context of an exponential characteristic of `R`, this theorem essentially asserts the defining property of the Frobenius map.
More concisely: For any commutative semiring `R` and natural number `p`, the Frobenius map ( raising to the power `p`) on an element `x` in `R` is equal to `x` raised to the power `p`.
|