map₂_eq_span_image2 — Mathlib

English

The submodule map₂ f p q equals the span of all f(m,n) with m ∈ p and n ∈ q.

Русский

Подмодуль map₂ f p q равен спектру всех элементов f(m,n) при m ∈ p, n ∈ q.

LaTeX

$$map₂ f p q = \\operatorname{span} R (\\operatorname{image2} (fun m n => LinearMap.instFunLike.coe (LinearMap.instFunLike.coe f m) n) p q)$$

Lean4

theorem map₂_eq_span_image2 (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    map₂ f p q = span R (Set.image2 (fun m n => f m n) (p : Set M) (q : Set N)) := by
  rw [← map₂_span_span, span_eq, span_eq]

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