Commit 2022-04-07 14:25 ac5188dd

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.