α : Type ?u.556480
M : Type u_4
N : Type u_5
P : Type ?u.556489
R : Type u_3
S : Type ?u.556495
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
κ : Type u_2
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
k : κ
n : N
⊢ ↑(lcongr e₁ e₂) (↑(LinearEquiv.symm (lcongr e₁ e₂)) (single k n)) =
    ↑(lcongr e₁ e₂) (single (↑e₁.symm k) (↑(LinearEquiv.symm e₂) n))
α : Type ?u.556480
M : Type u_4
N : Type u_5
P : Type ?u.556489
R : Type u_3
S : Type ?u.556495
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
κ : Type u_2
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
k : κ
n : N
⊢ ↑(LinearEquiv.symm (lcongr e₁ e₂)) (single k n) = single (↑e₁.symm k) (↑(LinearEquiv.symm e₂) n)
apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective
no goals
α : Type ?u.556480
M : Type u_4
N : Type u_5
P : Type ?u.556489
R : Type u_3
S : Type ?u.556495
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
κ : Type u_2
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
k : κ
n : N
⊢ ↑(lcongr e₁ e₂) (↑(LinearEquiv.symm (lcongr e₁ e₂)) (single k n)) =
    ↑(lcongr e₁ e₂) (single (↑e₁.symm k) (↑(LinearEquiv.symm e₂) n))
simp