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
characterstic, cardinality, ring
p is a unit in a commutative ring
R of nonzero characterstic iff it does not divide
p is a unit in a finite commutative ring
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.
A prime that does not divide the cardinality of a finite commutative ring
is a unit in