castNum_ldiff — Mathlib

English

The cast preserves ldiff: (ldiff m n) cast equals (cast m) ldiff (cast n).

Русский

Приведение сохраняет ldiff: cast(m ldif n) = cast(m) ldif cast(n).

LaTeX

$$$\mathrm{castNum}(\mathrm{ldiff}\, m\, n) = (\mathrm{castNum}\, m) \mathrm{ldiff} (\mathrm{castNum}\, n)$$$

Lean4

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

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