R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑Dfinsupp.equivFunOnFintype.symm (Pi.single i m) = ↑(lof R ι M i) m
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑(LinearEquiv.symm (linearEquivFunOnFintype R ι M)) (Pi.single i m) = ↑(lof R ι M i) m
change (Dfinsupp.equivFunOnFintype.symm (Pi.single i m)) = _
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ Dfinsupp.single i m = ↑(lof R ι M i) m
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑Dfinsupp.equivFunOnFintype.symm (Pi.single i m) = ↑(lof R ι M i) m
rw [Dfinsupp.equivFunOnFintype_symm_single i m]
no goals
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ Dfinsupp.single i m = ↑(lof R ι M i) m
rfl