induction_on — Mathlib

English

Induction principle applied to PiTensorProduct with explicit simp lemmas for smul and add steps.

Русский

Применение принципа индукции к PiTensorProduct с явными вспомогательными леммами для умножения на скаляр и сложения.

LaTeX

$$$$ \text{induction_on}(z,smul_tprod,add) $$$$

Lean4

/-- Induct using scaled versions of `PiTensorProduct.tprod`. -/
@[elab_as_elim]
protected theorem induction_on {motive : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
    (smul_tprod : ∀ (r : R) (f : Π i, s i), motive (r • tprod R f))
    (add : ∀ x y, motive x → motive y → motive (x + y)) : motive z :=
  by
  simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod
  exact PiTensorProduct.induction_on' z smul_tprod add

Похожие утверждения