Documentation

Mathlib.Algebra.CharP.CharAndCard

Characteristic and cardinality #

We prove some results relating characteristic and cardinality of finite rings

Tags #

characteristic, cardinality, ring

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] :

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

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) :

A prime that does not divide the cardinality of a finite commutative ring R is 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