feat(linear_algebra): generalize linear_equiv.finrank_eq to rings (#…

…12358)

Since `finrank` doesn't assume the module is actually a vector space, neither should the statement that linear equivalences preserve it.

src/linear_algebra/finite_dimensional.lean

@@ -793,23 +793,16 @@ protected theorem finite_dimensional (f : V ≃ₗ[K] V₂) [finite_dimensional
   finite_dimensional K V₂ :=
 module.finite.equiv f
 
+variables {R M M₂ : Type*} [ring R] [add_comm_group M] [add_comm_group M₂]
+variables [module R M] [module R M₂]
+
 /-- The dimension of a finite dimensional space is preserved under linear equivalence. -/
-theorem finrank_eq (f : V ≃ₗ[K] V₂) :
-  finrank K V = finrank K V₂ :=
-begin
-  by_cases h : finite_dimensional K V,
-  { resetI,
-    haveI : finite_dimensional K V₂ := f.finite_dimensional,
-    simpa [← finrank_eq_dim] using f.lift_dim_eq },
-  { rw [finrank_of_infinite_dimensional h, finrank_of_infinite_dimensional],
-    contrapose! h,
-    resetI,
-    exact f.symm.finite_dimensional }
-end
+theorem finrank_eq (f : M ≃ₗ[R] M₂) : finrank R M = finrank R M₂ :=
+by { unfold finrank, rw [← cardinal.to_nat_lift, f.lift_dim_eq, cardinal.to_nat_lift] }
 
 /-- Pushforwards of finite-dimensional submodules along a `linear_equiv` have the same finrank. -/
-lemma finrank_map_eq (f : V ≃ₗ[K] V₂) (p : submodule K V) :
-  finrank K (p.map (f : V →ₗ[K] V₂)) = finrank K p :=
+lemma finrank_map_eq (f : M ≃ₗ[R] M₂) (p : submodule R M) :
+  finrank R (p.map (f : M →ₗ[R] M₂)) = finrank R p :=
 (f.submodule_map p).finrank_eq.symm
 
 end linear_equiv