mathlib

2fae5fd7 - feat(algebra/char_p): use `finite` instead of `fintype` (#16002)

feat(algebra/char_p): use `finite` instead of `fintype` (#16002) * rename `char_ne_zero_of_fintype` to `char_ne_zero_of_finite`, use `[finite _]`; * rename `ring_char_ne_zero_of_fintype` to `ring_char_ne_zero_of_finite`, use `[finite _]`; * split `is_unit_iff_not_dvd_char_of_ring_char_ne_zero` from the proof of `is_unit_iff_not_dvd_char`; * add aliases `is_coprime.nat_coprime` and `nat.coprime.is_coprime`.