xor_right_injective

Mathlib.Data.Nat.Bitwise

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

← MathLib Explorer

English

For a fixed n, the function m ↦ (n ⊕ m) is injective.

Русский

Для фиксированного n функция m ↦ (n ⊕ m) инъективна.

LaTeX

$$$ \text{Injective}(\lambda m. n \oplus m) $$$

Lean4

theorem xor_right_injective {n : ℕ} : Function.Injective (HXor.hXor n : ℕ → ℕ) := fun m m' h => by
  rw [← xor_cancel_left n m, ← xor_cancel_left n m', h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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