mathlib documentation

core / init.data.char.lemmas

theorem char.val_of_nat_eq_of_is_valid {n : ℕ} :

is_valid_char n → (char.of_nat n).val = n

theorem char.val_of_nat_eq_of_not_is_valid {n : ℕ} :

¬is_valid_char n → (char.of_nat n).val = 0

theorem char.of_nat_eq_of_not_is_valid {n : ℕ} :

¬is_valid_char n → char.of_nat n = '\x00'

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

char.of_nat n₁ ≠ char.of_nat n₂