case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑↑(↑(generalLinearEquiv R M) f) x✝ = ↑↑f x✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ↑(↑(generalLinearEquiv R M) f) = ↑f
ext
no goals
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑↑(↑(generalLinearEquiv R M) f) x✝ = ↑↑f x✝
rfl