Commit 2022-08-11 16:08 2fae5fd7

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.