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

source
theorem is_unit_iff_not_dvd_char_of_ring_char_ne_zero (R : Type u_1) [comm_ring R] (p : ℕ) [fact (nat.prime p)] (hR : ring_char R ≠ 0) :
is_unit ↑p ↔ ¬p ∣ ring_char R

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

source
theorem is_unit_iff_not_dvd_char (R : Type u_1) [comm_ring R] (p : ℕ) [fact (nat.prime p)] [finite R] :
is_unit ↑p ↔ ¬p ∣ ring_char R

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

source
theorem prime_dvd_char_iff_dvd_card {R : Type u_1} [comm_ring R] [fintype R] (p : ℕ) [fact (nat.prime p)] :
p ∣ ring_char R ↔ p ∣ fintype.card R

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

source
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) :
¬is_unit ↑p

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