chore: flip and rename rank_eq_of_injective (#6301)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Aug 3, 2023 · 966fdb6 · 966fdb6
1 parent 68a37cd
commit 966fdb6
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean
@@ -406,7 +406,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     apply dim_V
   have dim_add : dim (W ⊔ img) + dim (W ⊓ img) = dim W + 2 ^ m := by
     convert ← Submodule.rank_sup_add_rank_inf_eq W img
-    rw [← rank_eq_of_injective (g m) g_injective]
+    rw [rank_range_of_injective (g m) g_injective]
     apply dim_V
   have dimW : dim W = card H := by
     have li : LinearIndependent ℝ (H.restrict e) := by

diff --git a/Mathlib/LinearAlgebra/Dimension.lean b/Mathlib/LinearAlgebra/Dimension.lean
@@ -198,10 +198,10 @@ theorem LinearEquiv.rank_eq (f : M ≃ₗ[R] M₁) : Module.rank R M = Module.ra
   Cardinal.lift_inj.1 f.lift_rank_eq
 #align linear_equiv.rank_eq LinearEquiv.rank_eq
 
-theorem rank_eq_of_injective (f : M →ₗ[R] M₁) (h : Injective f) :
-    Module.rank R M = Module.rank R (LinearMap.range f) :=
-  (LinearEquiv.ofInjective f h).rank_eq
-#align rank_eq_of_injective rank_eq_of_injective
+theorem rank_range_of_injective (f : M →ₗ[R] M₁) (h : Injective f) :
+    Module.rank R (LinearMap.range f) = Module.rank R M :=
+  (LinearEquiv.ofInjective f h).rank_eq.symm
+#align rank_eq_of_injective rank_range_of_injective
 
 /-- Pushforwards of submodules along a `LinearEquiv` have the same dimension. -/
 theorem LinearEquiv.rank_map_eq (f : M ≃ₗ[R] M₁) (p : Submodule R M) :

diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -891,9 +891,9 @@ variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCom
 /-- On a finite-dimensional space, an injective linear map is surjective. -/
 theorem surjective_of_injective [FiniteDimensional K V] {f : V →ₗ[K] V} (hinj : Injective f) :
     Surjective f := by
-  have h := rank_eq_of_injective _ hinj
+  have h := rank_range_of_injective _ hinj
   rw [← finrank_eq_rank, ← finrank_eq_rank, natCast_inj] at h
-  exact range_eq_top.1 (eq_top_of_finrank_eq h.symm)
+  exact range_eq_top.1 (eq_top_of_finrank_eq h)
 #align linear_map.surjective_of_injective LinearMap.surjective_of_injective
 
 /-- The image under an onto linear map of a finite-dimensional space is also finite-dimensional. -/

diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean
@@ -621,7 +621,7 @@ theorem rank_pow_quot_aux [IsDomain S] [IsDedekindDomain S] [p.IsMaximal] [P.IsP
       Module.rank (R ⧸ p) (S ⧸ P) +
         Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1))) := by
   letI : Field (R ⧸ p) := Ideal.Quotient.field _
-  rw [rank_eq_of_injective _ (powQuotSuccInclusion_injective f p P i),
+  rw [← rank_range_of_injective _ (powQuotSuccInclusion_injective f p P i),
     (quotientRangePowQuotSuccInclusionEquiv f p P hP0 hi).symm.rank_eq]
   exact (rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion f p P i))).symm
 #align ideal.rank_pow_quot_aux Ideal.rank_pow_quot_aux