Theorems · Theorem · linear algebra

PiTensorProduct.induction_on

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {motive : (PiTensorProduct R fun i => s i) → Prop}
  (z : PiTensorProduct R fun i => s i),
  (∀ (r : R) (f : (i : ι) → s i), motive (r • (PiTensorProduct.tprod R) f)) →
    (∀ (x y : PiTensorProduct R fun i => s i), motive x → motive y → motive (x + y)) → motive z

Induct using scaled versions of PiTensorProduct.tprod.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

6 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule