-rw-r--r-- 726 leangoppa-20230726/Goppadecoding/prod.lean raw
import Mathlib.Tactic

open BigOperators

namespace Goppadecoding

section lemmas_prod

theorem prod_filter_not_mul_prod_filter {U: Type _} {M: Type _} [CommMonoid M] (S: Finset U) (p: U → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] (f: U → M):
  (∏ x in S.filter (fun x ↦ ¬p x), f x) * (∏ x in S.filter p, f x) = ∏ x in S, f x := by
    rw[mul_comm]
    apply Finset.prod_filter_mul_prod_filter_not

theorem prod_eq_disjoint_union {U: Type _} {M: Type _} [CommMonoid M] [DecidableEq U] {A B C: Finset U} (union: C = A ∪ B) (disjoint: Disjoint A B) (f: U → M):
  ∏ x in C, f x = (∏ x in A, f x) * (∏ x in B, f x) := by
    rw[← Finset.prod_union disjoint]
    simp only[union]

end lemmas_prod