Theorems · Definition · linear algebra

LinearEquiv.piCongrRight

{R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type u_1} →
        {ψ : ι → Type u_2} →
          [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_2 : (i : ι) → Module R (φ i)] →
              [inst_3 : (i : ι) → AddCommMonoid (ψ i)] →
                [inst_4 : (i : ι) → Module R (ψ i)] → ((i : ι) → φ i ≃ₗ[R] ψ i) → ((i : ι) → φ i) ≃ₗ[R] (i : ι) → ψ i

Combine a family of linear equivalences into a linear equivalence of pi-types. This is Equiv.piCongrRight as a LinearEquiv

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

16 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule