Lemmas about bilinear maps with a basis over each argument #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
linear_map.ext_basis
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{R : Type u_3}
{R₂ : Type u_4}
{S : Type u_5}
{S₂ : Type u_6}
{M : Type u_7}
{N : Type u_8}
{P : Type u_9}
[comm_semiring R]
[comm_semiring S]
[comm_semiring R₂]
[comm_semiring S₂]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(b₁ : basis ι₁ R M)
(b₂ : basis ι₂ S N)
{B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(h : ∀ (i : ι₁) (j : ι₂), ⇑(⇑B (⇑b₁ i)) (⇑b₂ j) = ⇑(⇑B' (⇑b₁ i)) (⇑b₂ j)) :
B = B'
Two bilinear maps are equal when they are equal on all basis vectors.
theorem
linear_map.sum_repr_mul_repr_mulₛₗ
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{R : Type u_3}
{R₂ : Type u_4}
{S : Type u_5}
{S₂ : Type u_6}
{M : Type u_7}
{N : Type u_8}
{P : Type u_9}
[comm_semiring R]
[comm_semiring S]
[comm_semiring R₂]
[comm_semiring S₂]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(b₁ : basis ι₁ R M)
(b₂ : basis ι₂ S N)
{B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(x : M)
(y : N) :
Write out B x y as a sum over B (b i) (b j) if b is a basis.
Version for semi-bilinear maps, see sum_repr_mul_repr_mul for the bilinear version.
theorem
linear_map.sum_repr_mul_repr_mul
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{R : Type u_3}
{Mₗ : Type u_10}
{Nₗ : Type u_11}
{Pₗ : Type u_12}
[comm_semiring R]
[add_comm_monoid Mₗ]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R Mₗ]
[module R Nₗ]
[module R Pₗ]
(b₁' : basis ι₁ R Mₗ)
(b₂' : basis ι₂ R Nₗ)
{B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ}
(x : Mₗ)
(y : Nₗ) :
Write out B x y as a sum over B (b i) (b j) if b is a basis.
Version for bilinear maps, see sum_repr_mul_repr_mulₛₗ for the semi-bilinear version.