digits_inj_iff

Mathlib.Data.Nat.Digits.Defs

URI: https://scilib.ai/kg/mathlib#Nat.digits_inj_iff

English

For all base b and natural numbers n, m, digits_b(n) = digits_b(m) if and only if n = m.

Русский

Для любой базы b и чисел n, m верно: digits_b(n) = digits_b(m) тогда и только тогда, когда n = m.

LaTeX

$$$ \forall b\, n\, m:\ (digits_b(n) = digits_b(m)) \iff n = m $$$

Lean4

@[simp]
theorem digits_inj_iff {b n m : ℕ} : b.digits n = b.digits m ↔ n = m :=
  (digits.injective b).eq_iff

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru