English
There is an induction principle for IsTensorProduct: if P is a property of elements of M, and P(0) holds, and P(f x y) holds for all x,y, and P is closed under addition, then P holds for every m ∈ M.
Русский
Существует принцип индукции по IsTensorProduct: если P свойство для элементов M, P(0) истинно, P(f x y) для всех x,y истинно, и P сохраняется при сложении, тогда P выполняется для любого m ∈ M.
LaTeX
$$IsTensorProduct.inductionOn (h : IsTensorProduct f) (m : M) (zero : motive 0) (tmul : ∀ x y, motive (f x y)) (add : ∀ x y, motive x → motive y → motive (x + y))$$
Lean4
/-- Given a bilinear map `f : M₁ →ₗ[R] M₂ →ₗ[R] M`, `IsTensorProduct f` means that
`M` is the tensor product of `M₁` and `M₂` via `f`.
This is defined by requiring the lift `M₁ ⊗[R] M₂ → M` to be bijective.
-/
def IsTensorProduct : Prop :=
Function.Bijective (TensorProduct.lift f)
