Theorems · Theorem · linear algebra

DFinsupp.mapRange.linearEquiv_symm

∀ {ι : 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)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i),
  (DFinsupp.mapRange.linearEquiv e).symm = DFinsupp.mapRange.linearEquiv fun i => (e i).symm

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule