mathlib documentation

core / init.data.char.lemmas

theorem char.of_nat_ne_of_ne {n₁ n₂ : } (h₁ : n₁ n₂) (h₂ : is_valid_char n₁) (h₃ : is_valid_char n₂) :