rainbow.math.sums.period-usage

Finite sums src/rainbow/math/sums/period_usage.clj0 definitions, 1 theorems

Multiplying two Boolean indicators by a weight equals filtering that weight by both tests.

signed/two-indicator-weight-is-filtered

TheoremFor all inputsNo axiomsSource

signed/two-indicator-weight-is-filtered :
  (A B : data/Bool) (r : ℚ)
  → data/Bool.rec (fun x₄ => ℚ) 0 1 A · data/Bool.rec (fun x₈ => ℚ) 0 1 B · r = data/Bool.rec (fun x₂₀ => ℚ) 0 (data/Bool.rec (fun x₂₄ => ℚ) 0 r B) A

0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational