Theorems · Definition · linear algebra

DFinsupp.mapRange.linearEquiv

{ι : Type u_1} →
  {R : Type u_3} →
    [inst : Semiring R] →
      {β₁ : ι → Type u_8} →
        {β₂ : ι → Type u_9} →
          [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] →
            [inst_2 : (i : ι) → AddCommMonoid (β₂ i)] →
              [inst_3 : (i : ι) → Module R (β₁ i)] →
                [inst_4 : (i : ι) → Module R (β₂ i)] →
                  ((i : ι) → β₁ i ≃ₗ[R] β₂ i) → (Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i

DFinsupp.mapRange.linearMap as a LinearEquiv.

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

7 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule