Theorems · Definition · linear algebra

LinearEquiv.piRing

(R : Type u) →
  (M : Type v) →
    (ι : Type x) →
      [inst : Semiring R] →
        (S : Type u_4) →
          [Fintype ι] →
            [DecidableEq ι] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module S M] → [inst_7 : SMulCommClass R S M] → ((ι → R) →ₗ[R] M) ≃ₗ[S] ι → M

Linear equivalence between linear functions Rⁿ → M and Mⁿ. The spaces Rⁿ and Mⁿ are represented as ι → R and ι → M, respectively, where ι is a finite type. This as an S-linear equivalence, under the assumption that S acts on M commuting with R. When R is commutative, we can take this to be the usual action with S = R. Otherwise, S = ℕ shows that the equivalence is additive. See note [bundled maps over different rings].

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

3 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringFintypeDecidableEqSemiringAddCommMonoidModuleModuleSMulCommClass