mathlib documentation

core.init.data.char.lemmas

theorem char.of_nat_ne_of_ne {n₁ n₂ : } :
n₁ n₂is_valid_char n₁is_valid_char n₂char.of_nat n₁ char.of_nat n₂