English
IsTensorProduct.inductionOn provides an induction principle for IsTensorProduct: if P holds for 0, for simple tensors, and is additive, then P holds for all elements.
Русский
IsTensorProduct.inductionOn даёт принцип индукции для IsTensorProduct: если P выполняется для 0, для простых тензоров и при сложении, то P выполняется для всех элементов.
LaTeX
$$IsTensorProduct.inductionOn (h : IsTensorProduct f) {motive : M → Prop} (m : M) (zero : motive 0) (tmul : ∀ x y, motive (f x y)) (add : ∀ x y, motive x → motive y → motive (x + y)) : motive m$$
Lean4
@[elab_as_elim]
theorem inductionOn (h : IsTensorProduct f) {motive : M → Prop} (m : M) (zero : motive 0) (tmul : ∀ x y, motive (f x y))
(add : ∀ x y, motive x → motive y → motive (x + y)) : motive m :=
by
rw [← h.equiv.right_inv m]
generalize h.equiv.invFun m = y
change motive (TensorProduct.lift f y)
induction y with
| zero => rwa [map_zero]
| tmul _ _ =>
rw [TensorProduct.lift.tmul]
apply tmul
| add _ _ _ _ =>
rw [map_add]
apply add <;> assumption
