Characteristic and cardinality

We prove some results relating characteristic and cardinality of finite rings

Tags

characteristic, cardinality, ring

theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] (hR : ringChar R ≠ 0) : IsUnit ↑p ↔ ¬p ∣ ringChar R

A prime p is a unit in a commutative ring R of nonzero characteristic iff it does not divide the characteristic.

theorem isUnit_iff_not_dvd_char (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Finite R] : IsUnit ↑p ↔ ¬p ∣ ringChar R

A prime p is a unit in a finite commutative ring R iff it does not divide the characteristic.

theorem prime_dvd_char_iff_dvd_card {R : Type u_1} [CommRing R] [Fintype R] (p : ℕ) [Fact (Nat.Prime p)] : p ∣ ringChar R ↔ p ∣ Fintype.card R

The prime divisors of the characteristic of a finite commutative ring are exactly the prime divisors of its cardinality.

theorem not_isUnit_prime_of_dvd_card {R : Type u_1} [CommRing R] [Fintype R] {p : ℕ} [Fact (Nat.Prime p)] (hp : p ∣ Fintype.card R) : ¬IsUnit ↑p

A prime that divides the cardinality of a finite commutative ring R isn't a unit in R.

theorem charP_of_card_eq_prime {R : Type u_1} [NonAssocRing R] [Fintype R] {p : ℕ} [hp : Fact (Nat.Prime p)] (hR : Fintype.card R = p) : CharP R p

theorem charP_of_card_eq_prime_pow {R : Type u_1} [CommRing R] [IsDomain R] [Fintype R] {p f : ℕ} [hp : Fact (Nat.Prime p)] (hR : Fintype.card R = p ^ f) : CharP R p