English
The infinite product over β of a fixed element a equals a raised to the power equal to the cardinality of β: ∏'_{β} a = a^{|β|}.
Русский
Бесконечное произведение по β фиксированного элемента a равно a в степени кардинальности β: ∏'_{β} a = a^{|β|}.
LaTeX
$$$$ \prod' _{\beta} a = a^{|\beta|}. $$$$
Lean4
@[to_additive (attr := simp)]
theorem tprod_const [T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β) :=
by
rcases finite_or_infinite β with hβ | hβ
· letI : Fintype β := Fintype.ofFinite β
rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]
simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]
· simp only [Nat.card_eq_zero_of_infinite, pow_zero]
rcases eq_or_ne a 1 with rfl | ha
· simp
· apply tprod_eq_one_of_not_multipliable
simpa [multipliable_const_iff] using ha
