of_equiv — Mathlib

English

If there is an isomorphism e: M1 ⊗ M2 ≃ M and a compatibility condition with f, then IsTensorProduct f holds.

Русский

Если существует изоморфизм e: M1 ⊗ M2 ≃ M и выполняется совместимость с f, тогда IsTensorProduct f выполняется.

LaTeX

$$IsTensorProduct.of_equiv e he$$

Lean4

theorem of_equiv (e : M₁ ⊗[R] M₂ ≃ₗ[R] M) (he : ∀ x y, e (x ⊗ₜ y) = f x y) : IsTensorProduct f :=
  by
  have : TensorProduct.lift f = e := by
    ext x y
    simp [he]
  simpa [IsTensorProduct, this] using e.bijective

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