Documentation

Mathlib.Algebra.CharP.CharAndCard

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 p.Prime] (hR : ringChar R 0) :

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 p.Prime] [Finite 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 p.Prime] :

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 p.Prime] (hp : p Fintype.card R) :

A prime that does not divide the cardinality of a finite commutative ring R is a unit in R.