mathlib3 documentation

algebra.char_p.char_and_card

Characteristic and cardinality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove some results relating characteristic and cardinality of finite rings

Tags #

characterstic, cardinality, ring

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

theorem is_unit_iff_not_dvd_char (R : Type u_1) [comm_ring 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.

theorem prime_dvd_char_iff_dvd_card {R : Type u_1} [comm_ring R] [fintype R] (p : ) [fact (nat.prime p)] :

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

theorem not_is_unit_prime_of_dvd_card {R : Type u_1} [comm_ring 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.