isUnit_iff_not_dvd_char_of_ringChar_ne_zero
theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero :
∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [inst_1 : Fact p.Prime],
ringChar R ≠ 0 → (IsUnit ↑p ↔ ¬p ∣ ringChar R)
The theorem `isUnit_iff_not_dvd_char_of_ringChar_ne_zero` states that for any commutative ring `R` of nonzero characteristic and any prime number `p`, `p` is a unit in `R` if and only if `p` does not divide the characteristic of `R`. In other words, a prime number is a unit (it has a multiplicative inverse) in a given commutative ring with nonzero characteristic precisely when the prime number doesn't divide the ring's characteristic.
More concisely: A prime number `p` is a unit in a commutative ring `R` of nonzero characteristic if and only if `p` does not divide the characteristic of `R`.
|
isUnit_iff_not_dvd_char
theorem isUnit_iff_not_dvd_char :
∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [inst_1 : Fact p.Prime] [inst_2 : Finite R],
IsUnit ↑p ↔ ¬p ∣ ringChar R
The theorem `isUnit_iff_not_dvd_char` states that for any given finite commutative ring `R` and a prime number `p`, the prime number `p` is a unit in `R` if and only if `p` does not divide the characteristic of the ring `R`. In other words, the primality of `p` in the ring `R` is contingent upon `p` not being a factor of the ring's characteristic.
More concisely: A prime number `p` is a unit in a finite commutative ring `R` if and only if `p` does not divide the characteristic of `R`.
|
prime_dvd_char_iff_dvd_card
theorem prime_dvd_char_iff_dvd_card :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fintype R] (p : ℕ) [inst_2 : Fact p.Prime],
p ∣ ringChar R ↔ p ∣ Fintype.card R
The theorem `prime_dvd_char_iff_dvd_card` states that for any finite commutative ring `R` and any prime number `p`, `p` divides the characteristic of the ring `R` if and only if `p` divides the cardinality (the number of elements) of `R`. In other words, the prime divisors of the characteristic of a finite commutative ring are exactly the same as the prime divisors of its cardinality.
More concisely: A finite commutative ring's characteristic is a prime number if and only if that prime number is a divisor of the ring's cardinality.
|
not_isUnit_prime_of_dvd_card
theorem not_isUnit_prime_of_dvd_card :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fintype R] (p : ℕ) [inst_2 : Fact p.Prime],
p ∣ Fintype.card R → ¬IsUnit ↑p
The theorem `not_isUnit_prime_of_dvd_card` states that for any finite commutative ring `R`, if a prime number `p` divides the cardinality (i.e., the number of elements) of `R`, then `p` is not a unit in `R`. In other words, if a prime number `p` exactly divides the size of a finite commutative ring `R`, then `p` does not have a multiplicative inverse in `R`.
More concisely: In a finite commutative ring, a prime number that divides the ring's cardinality is not a multiplicative unit.
|