English
PiTensorProduct inherits an additive commutative monoid structure from its components.
Русский
PiTensorProduct наследует структуру коммутативного моноида сложения от своих компонентов.
LaTeX
$$AddCommMonoid (PiTensorProduct R (fun i => s i))$$
Lean4
/-- Induct using `tprodCoeff` -/
@[elab_as_elim]
protected theorem induction_on' {motive : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
(tprodCoeff : ∀ (r : R) (f : Π i, s i), motive (tprodCoeff R r f))
(add : ∀ x y, motive x → motive y → motive (x + y)) : motive z :=
by
have C0 : motive 0 := by
have h₁ := tprodCoeff 0 0
rwa [zero_tprodCoeff] at h₁
refine AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 ?_
simp_rw [AddCon.coe_add]
refine fun f y ih ↦ add _ _ ?_ ih
convert tprodCoeff f.1 f.2
