K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ ↑toNat (Module.rank R M) = ↑toNat (Module.rank R M₂)
K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ finrank R M = finrank R M₂
unfold finrank
no goals
K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ ↑toNat (Module.rank R M) = ↑toNat (Module.rank R M₂)
rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]