mathlib3

ac5188dd - chore(algebra/char_p/{basic + algebra}): weaken assumptions for char_p_to_char_zero (#13214)

chore(algebra/char_p/{basic + algebra}): weaken assumptions for char_p_to_char_zero (#13214) The assumptions for lemma `char_p_to_char_zero` can be weakened, without changing the proof. Since the weakening breaks up one typeclass assumption into two, when the lemma was applied with `@`, I inserted an extra `_`. This happens twice: once in the file where the lemma is, and once in a separate file.