case a
ι : Type u_1
ι' : Type u_4
R : Type u_2
R₂ : Type ?u.557598
K : Type ?u.557601
M : Type u_3
M' : Type u_5
M'' : Type ?u.557610
V : Type u
V' : Type ?u.557615
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b✝ b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b'✝ : Basis ι' R M'
e✝ : ι ≃ ι'
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι
⊢ ↑(Basis.map b (Basis.equiv b b' e)) i = ↑(reindex b' e.symm) i
ι : Type u_1
ι' : Type u_4
R : Type u_2
R₂ : Type ?u.557598
K : Type ?u.557601
M : Type u_3
M' : Type u_5
M'' : Type ?u.557610
V : Type u
V' : Type ?u.557615
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x : M
b'✝ : Basis ι' R M'
e✝ : ι ≃ ι'
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ Basis.map b (Basis.equiv b b' e) = reindex b' e.symm
ext i
no goals
case a
ι : Type u_1
ι' : Type u_4
R : Type u_2
R₂ : Type ?u.557598
K : Type ?u.557601
M : Type u_3
M' : Type u_5
M'' : Type ?u.557610
V : Type u
V' : Type ?u.557615
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b✝ b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b'✝ : Basis ι' R M'
e✝ : ι ≃ ι'
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι
⊢ ↑(Basis.map b (Basis.equiv b b' e)) i = ↑(reindex b' e.symm) i
simp