R : Type u_1
A : Type ?u.386467
B : Type ?u.386470
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hM : Finite R M
f : M →ₗ[R] N
hf : Surjective ↑f
⊢ Submodule.FG (Submodule.map f ⊤)
R : Type u_1
A : Type ?u.386467
B : Type ?u.386470
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hM : Finite R M
f : M →ₗ[R] N
hf : Surjective ↑f
⊢ Submodule.FG ⊤
rw [← LinearMap.range_eq_top.2 hf, ← Submodule.map_top]
no goals
R : Type u_1
A : Type ?u.386467
B : Type ?u.386470
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hM : Finite R M
f : M →ₗ[R] N
hf : Surjective ↑f
⊢ Submodule.FG (Submodule.map f ⊤)
exact hM.1.map f