castNum_and — Mathlib

English

The cast preserves bitwise AND: for all m,n, cast(m &&& n) = cast(m) &&& cast(n).

Русский

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

LaTeX

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

Lean4

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

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