English
For a commutative group G and a decidable equality on A, the product over a list l after replacing each element by either f x or g x depending on whether x=a equals the product where you fix the a-case with a power and multiply by the product of g over l.
Русский
Для группы G иDecidableEq на A, произведение по списку l после подстановки для каждого элемента либо f x, либо g x в зависимости от x=a равно произведению, где учтён случай a в виде степени, умноженному на произведение g по l.
LaTeX
$$$(l.map (\x => if x = a then f x else g x)).prod = \left( \frac{f a}{g a} \right)^{l.count a} \cdot (l.map g).prod$$
Lean4
@[to_additive]
theorem prod_map_ite_eq {A : Type*} [DecidableEq A] (l : List A) (f g : A → G) (a : A) :
(l.map fun x => if x = a then f x else g x).prod = (f a / g a) ^ (l.count a) * (l.map g).prod := by
induction l with
| nil => simp
| cons x xs ih =>
simp only [map_cons, prod_cons, count_cons] at ih ⊢
rw [ih]
clear ih
by_cases hx : x = a
·
simp only [hx, ite_true, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm,
mul_inv_cancel_left, beq_self_eq_true]
· simp only [hx, ite_false, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]
