English
Given a finite index set and a family of elements in a commutative group with zero, the mk0 of the product equals the product of mk0s over attached indices (with a suitable clause on zeros).
Русский
Для конечного множителя и семейства элементов в коммутативной группе с нулём равенство: mk0 произведения по i эквивалентно произведению mk0 элементов по сопряжённым индексам (с условиями на нули).
LaTeX
$$$\\forall {ι} {G₀} [\\mathsf{CommGroupWithZero} G₀] (s:\\mathsf{Finset} ι) (f: ι \\to G₀) (h),\\; \\mathrm{Units.mk0}\\left(\\prod i\\in s, f i\\right) h = \\prod i\\in s.\\mathrm{attach}, \\mathrm{Units.mk0}(f i) \\, (\\text{...})$$$
Lean4
theorem mk0_prod [CommGroupWithZero G₀] (s : Finset ι) (f : ι → G₀) (h) :
Units.mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, Units.mk0 (f i) fun hh ↦ h (Finset.prod_eq_zero i.2 hh) := by
classical induction s using Finset.induction_on <;> simp [*]
