English
Replacement of the insert lemma with a prime variant, showing the same relation as insert_of_notMem but using a symmetrical form.
Русский
Замена леммы вставки с помощью варианта в виде prime, демонстрирующая ту же зависимость, что и insert_of_notMem, но симметричной формой.
LaTeX
$$$ noncommProd (insert a s) f comm = noncommProd s f (comm.mono (\; fun _ => mem_insert_of_mem)) * f a $$$
Lean4
@[to_additive]
theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
(univ.noncommProd (fun i => Pi.mulSingle i (x i)) fun i _ j _ _ => Pi.mulSingle_apply_commute x i j) = x :=
by
ext i
apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a (Pi.evalMonoidHom M i)).trans
case a =>
intro i _ j _ _
exact Pi.mulSingle_apply_commute x i j
convert (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _
· intro j
exact Pi.mulSingle j (x j) i
· intro j _; dsimp
· rw [noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _), noncommProd_eq_pow_card (univ.erase i), one_pow,
mul_one]
· simp only [Pi.mulSingle_eq_same]
· intro j hj
simp? at hj says simp only [mem_erase, ne_eq, mem_univ, and_true] at hj
simp only [Pi.mulSingle, Function.update, Pi.one_apply, dite_eq_right_iff]
intro h
simp [*] at *
