mathlib3

0ed425fa - feat(ring_theory/perfection): define characteristic predicate of perfection (#5386)

feat(ring_theory/perfection): define characteristic predicate of perfection (#5386) Name changes: - `perfect_field` --> `perfect_ring` (generalization) - `semiring.perfection` --> `ring.perfection` - Original `ring.perfection` deleted.