Documentation

Mathlib.LinearAlgebra.Basis.Prod

Bases for the product of modules #

source
🔸 coverage
noncomputable def Module.Basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') :
Basis (ι ⊕ ι') R (M × M')

Basis.prod maps an ι-indexed basis for M and an ι'-indexed basis for M' to an ι ⊕ ι'-index basis for M × M'. For the specific case of R × R, see also Basis.finTwoProd.

Instances For
    source
    📐 coverage
    @[simp]
    theorem Module.Basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (x : M × M') (i : ι) :
    ((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i
    source
    📐 coverage
    @[simp]
    theorem Module.Basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (x : M × M') (i : ι') :
    ((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i
    source
    📐 coverage
    theorem Module.Basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι) :
    ((b.prod b') (Sum.inl i)).1 = b i
    source
    📐 coverage
    theorem Module.Basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι') :
    ((b.prod b') (Sum.inr i)).1 = 0
    source
    📐 coverage
    theorem Module.Basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι) :
    ((b.prod b') (Sum.inl i)).2 = 0
    source
    📐 coverage
    theorem Module.Basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι') :
    ((b.prod b') (Sum.inr i)).2 = b' i
    source
    📐 coverage
    @[simp]
    theorem Module.Basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι ⊕ ι') :
    (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i
    source
    📐 coverage
    instance Module.Free.prod (R : Type u_7) (M : Type u_8) (N : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Free R M] [Free R N] :
    Free R (M × N)