refactor(linear_algebra/*): Rename linear_equiv.range to linear_equiv.range_eq_top

src/geometry/manifold/mfderiv.lean

@@ -1593,7 +1593,7 @@ lemma ker_mfderiv_eq_bot {x : M} (hx : x ∈ e.source) :
 
 lemma range_mfderiv_eq_top {x : M} (hx : x ∈ e.source) :
   linear_map.range (mfderiv I I' e x) = ⊤ :=
-(he.mfderiv hx).to_linear_equiv.range
+(he.mfderiv hx).to_linear_equiv.range_eq_top
 
 lemma range_mfderiv_eq_univ {x : M} (hx : x ∈ e.source) :
   range (mfderiv I I' e x) = univ :=

src/linear_algebra/basic.lean

@@ -1727,7 +1727,7 @@ include σ₂₁ re₁₂ re₂₁
 rfl
 omit σ₂₁ re₁₂ re₂₁
 
-@[simp] protected theorem range : (e : M →ₛₗ[σ₁₂] M₂).range = ⊤ :=
+@[simp] protected theorem range_eq_top : (e : M →ₛₗ[σ₁₂] M₂).range = ⊤ :=
 linear_map.range_eq_top.2 e.to_equiv.surjective
 
 include σ₂₁ re₁₂ re₂₁
@@ -1749,7 +1749,7 @@ linear_map.ker_eq_bot_of_injective e.to_equiv.injective
 @[simp] theorem range_comp [ring_hom_surjective σ₁₂] [ring_hom_surjective σ₂₃]
   [ring_hom_surjective σ₁₃] :
   (h.comp (e : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃).range = h.range :=
-linear_map.range_comp_of_range_eq_top _ e.range
+linear_map.range_comp_of_range_eq_top _ e.range_eq_top
 
 include module_M
 @[simp] theorem ker_comp (l : M →ₛₗ[σ₁₂] M₂) :

src/linear_algebra/basis.lean

@@ -157,7 +157,7 @@ by { rw ← b.coe_repr_symm, exact b.repr.apply_symm_apply v }
 by { rw ← b.coe_repr_symm, exact b.repr.symm_apply_apply x }
 
 lemma repr_range : (b.repr : M →ₗ[R] (ι →₀ R)).range = finsupp.supported R R univ :=
-by rw [linear_equiv.range, finsupp.supported_univ]
+by rw [linear_equiv.range_eq_top, finsupp.supported_univ]
 
 lemma mem_span_repr_support {ι : Type*} (b : basis ι R M) (m : M) :
   m ∈ span R (b '' (b.repr m).support) :=
@@ -541,7 +541,7 @@ b.constr_eq S $ λ x, rfl
 
 lemma constr_range [nonempty ι] {f : ι  → M'} :
   (b.constr S f).range = span R (range f) :=
-by rw [b.constr_def S f, linear_map.range_comp, linear_map.range_comp, linear_equiv.range,
+by rw [b.constr_def S f, linear_map.range_comp, linear_map.range_comp, linear_equiv.range_eq_top,
        ← finsupp.supported_univ, finsupp.lmap_domain_supported, ←set.image_univ,
        ← finsupp.span_image_eq_map_total, set.image_id]
 

src/linear_algebra/dual.lean

@@ -1067,7 +1067,7 @@ begin
   let f' := linear_map.quot_ker_equiv_of_surjective f hf,
   transitivity linear_map.range (f.dual_map.comp f'.symm.dual_map.to_linear_map),
   { rw linear_map.range_comp_of_range_eq_top,
-    apply linear_equiv.range },
+    apply linear_equiv.range_eq_top },
   { apply congr_arg,
     ext φ x,
     simp only [linear_map.coe_comp, linear_equiv.coe_to_linear_map, linear_map.dual_map_apply,

src/linear_algebra/finsupp.lean

@@ -933,8 +933,8 @@ variables {S}
 
 @[simp]
 lemma fintype.range_total : (fintype.total R S v).range = submodule.span R (set.range v) :=
-by rw [← finsupp.total_eq_fintype_total, linear_map.range_comp,
-  linear_equiv.to_linear_map_eq_coe, linear_equiv.range, submodule.map_top, finsupp.range_total]
+by rw [← finsupp.total_eq_fintype_total, linear_map.range_comp, linear_equiv.to_linear_map_eq_coe,
+  linear_equiv.range_eq_top, submodule.map_top, finsupp.range_total]
 
 section span_range
 

src/linear_algebra/linear_independent.lean

@@ -738,7 +738,7 @@ lemma linear_independent.repr_ker : hv.repr.ker = ⊥ :=
 by rw [linear_independent.repr, linear_equiv.ker]
 
 lemma linear_independent.repr_range : hv.repr.range = ⊤ :=
-by rw [linear_independent.repr, linear_equiv.range]
+by rw [linear_independent.repr, linear_equiv.range_eq_top]
 
 lemma linear_independent.repr_eq
   {l : ι →₀ R} {x} (eq : finsupp.total ι M R v l = ↑x) :