induction_on — Mathlib

English

The canonical map that sends a pair (m,n) to the tensor product m ⊗ n defines the bilinear map underlying the tensor product.

Русский

Каноническое отображение (m,n) ↦ m ⊗ n задаёт билинейное отображение, лежащее в основе тензорного произведения.

LaTeX

$$$ \\mathrm{tmul}(m,n) = m \\otimes_R n. $$$

Lean4

@[elab_as_elim, induction_eliminator]
protected theorem induction_on {motive : M ⊗[R] N → Prop} (z : M ⊗[R] N) (zero : motive 0)
    (tmul : ∀ x y, motive <| x ⊗ₜ[R] y) (add : ∀ x y, motive x → motive y → motive (x + y)) : motive z :=
  AddCon.induction_on z fun x =>
    FreeAddMonoid.recOn x zero fun ⟨m, n⟩ y ih => by
      rw [AddCon.coe_add]
      exact add _ _ (tmul ..) ih

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