ext' — Mathlib

English

For a bilinear f and a linear g, lifting f.compr₂ g equals g composed with lift f.

Русский

Для билинейного отображения f и линейного g переход через lift_compr₂ равен композиции g с lift f.

LaTeX

$$$\\mathrm{lift}(f.\\compr_2\\, g) = g \\circ (\\mathrm{lift}\\ f).$$$

Lean4

theorem ext' {g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
  LinearMap.ext fun z =>
    TensorProduct.induction_on z (by simp_rw [LinearMap.map_zero]) H fun x y ihx ihy => by
      rw [g.map_add, h.map_add, ihx, ihy]

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