xor_left_injective

Mathlib.Data.Nat.Bitwise

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem xor_left_injective {n : ℕ} : Function.Injective fun m => m ^^^ n := fun m m' (h : m ^^^ n = m' ^^^ n) => by
  rw [← xor_cancel_right n m, ← xor_cancel_right n m', h]

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

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

Разделы

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

Аффилиация

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