chore(linear_algebra/dimension): tidy lemma names for linear_map.rank (#18769)

`le1` and `le2` don't really fit the usual naming convention.

Also generalizes `rank_le_domain` to rings and `rank_le_range` across universes.

Author: eric-wieser

src/data/matrix/rank.lean

@@ -56,7 +56,7 @@ lemma rank_mul_le [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R
   (A ⬝ B).rank ≤ A.rank :=
 begin
   rw [rank, rank, to_lin'_mul],
-  refine cardinal.to_nat_le_of_le_of_lt_aleph_0 _ (linear_map.rank_comp_le1 _ _),
+  refine cardinal.to_nat_le_of_le_of_lt_aleph_0 _ (linear_map.rank_comp_le_left _ _),
   rw [←cardinal.lift_lt_aleph_0],
   have := lift_rank_range_le A.to_lin',
   rw [rank_fun', cardinal.lift_nat_cast] at this,

src/linear_algebra/dimension.lean

@@ -1317,15 +1317,18 @@ variables [add_comm_group V'] [module K V']
 /-- `rank f` is the rank of a `linear_map` `f`, defined as the dimension of `f.range`. -/
 def rank (f : V →ₗ[K] V') : cardinal := module.rank K f.range
 
-lemma rank_le_range (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V₁ :=
+lemma rank_le_range (f : V →ₗ[K] V') : rank f ≤ module.rank K V' :=
 rank_submodule_le _
 
+lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V :=
+rank_range_le _
+
 @[simp] lemma rank_zero [nontrivial K] : rank (0 : V →ₗ[K] V') = 0 :=
 by rw [rank, linear_map.range_zero, rank_bot]
 
 variables [add_comm_group V''] [module K V'']
 
-lemma rank_comp_le1 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f :=
+lemma rank_comp_le_left (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f :=
 begin
   refine rank_le_of_submodule _ _ _,
   rw [linear_map.range_comp],
@@ -1334,7 +1337,7 @@ end
 
 variables [add_comm_group V'₁] [module K V'₁]
 
-lemma rank_comp_le2 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g :=
+lemma rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g :=
 by rw [rank, rank, linear_map.range_comp]; exact rank_map_le _ _
 
 end ring
@@ -1343,9 +1346,6 @@ section division_ring
 variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
 variables [add_comm_group V'] [module K V']
 
-lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V :=
-by { rw [← rank_range_add_rank_ker f], exact self_le_add_right _ _ }
-
 lemma rank_add_le (f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g :=
 calc rank (f + g) ≤ module.rank K (f.range ⊔ g.range : submodule K V') :
   begin

src/linear_algebra/matrix/to_lin.lean

@@ -342,12 +342,13 @@ lemma linear_map.to_matrix_alg_equiv'_mul
   (f * g).to_matrix_alg_equiv' = f.to_matrix_alg_equiv' ⬝ g.to_matrix_alg_equiv' :=
 linear_map.to_matrix_alg_equiv'_comp f g
 
-lemma matrix.rank_vec_mul_vec {K m n : Type u} [field K] [fintype n] [decidable_eq n]
+lemma matrix.rank_vec_mul_vec {K m n : Type u}
+  [comm_ring K] [strong_rank_condition K] [fintype n] [decidable_eq n]
   (w : m → K) (v : n → K) :
   rank (vec_mul_vec w v).to_lin' ≤ 1 :=
 begin
   rw [vec_mul_vec_eq, matrix.to_lin'_mul],
-  refine le_trans (rank_comp_le1 _ _) _,
+  refine le_trans (rank_comp_le_left _ _) _,
   refine (rank_le_domain _).trans_eq _,
   rw [rank_fun', fintype.card_unit, nat.cast_one]
 end