mathlib3
053a03d6 - feat(algebra/char_p): `char_p` of a local ring is zero or prime power (#14461)

Commit

3 years ago

feat(algebra/char_p): `char_p` of a local ring is zero or prime power (#14461) For a local commutative ring the characteristics is either zero or a prime power.

Author

Jon Eugster

Parents

2e3a0a6e

mathlib3 053a03d6 - feat(algebra/char_p): `char_p` of a local ring is zero or prime power (#14461)

mathlib3
053a03d6 - feat(algebra/char_p): `char_p` of a local ring is zero or prime power (#14461)