castNum_xor — Mathlib

English

The cast preserves bitwise XOR: (m ^^^ n) cast equals cast(m) ^^^ cast(n).

Русский

Приведение сохраняет битовую операцию XOR: cast(m) XOR cast(n) = cast(m XOR n).

LaTeX

$$$((m \\^\\\^\\ n) : \\alpha) = (m : \\alpha) \\^\\\^ (n : \\alpha)$$$

Lean4

@[simp, norm_cast]
theorem castNum_xor : ∀ m n : Num, ↑(m ^^^ n) = (↑m ^^^ ↑n : ℕ) := by
  apply castNum_eq_bitwise PosNum.lxor <;> intros <;> (try cases_type* Bool) <;> rfl

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