Lemmas about bilinear maps with a basis over each argument #
theorem
LinearMap.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}
[Semiring R]
[Semiring S]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module S N]
[Module R₂ P]
[Module S₂ P]
[SMulCommClass 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
LinearMap.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}
[Semiring R]
[Semiring S]
[Semiring R₂]
[Semiring S₂]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module S N]
[Module R₂ P]
[Module S₂ P]
[SMulCommClass 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
LinearMap.sum_repr_mul_repr_mul
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{Rₗ : Type u_10}
{Mₗ : Type u_11}
{Nₗ : Type u_12}
{Pₗ : Type u_13}
[CommSemiring Rₗ]
[AddCommMonoid Mₗ]
[AddCommMonoid Nₗ]
[AddCommMonoid 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.