Apply suggestions from code review

Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/RingTheory/LinearDisjoint.lean

@@ -33,23 +33,23 @@ See the file `Mathlib/LinearAlgebra/LinearDisjoint.lean` for details.
 ### Equivalent characterization of linearly disjointness
 
 - `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat`:
-  if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of
+  if `A` and `B` are linearly disjoint, and if `B` is a flat `R`-module, then for any family of
   `R`-linearly independent elements of `A`, they are also `B`-linearly independent.
 
 - `Subalgebra.LinearDisjoint.of_basis_left_op`:
   conversely, if a basis of `A` is also `B`-linearly independent, then `A` and `B` are
   linearly disjoint.
 
 - `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat`:
-  if `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of
+  if `A` and `B` are linearly disjoint, and if `A` is a flat `R`-module, then for any family of
   `R`-linearly independent elements of `B`, they are also `A`-linearly independent.
 
 - `Subalgebra.LinearDisjoint.of_basis_right`:
   conversely, if a basis of `B` is also `A`-linearly independent,
   then `A` and `B` are linearly disjoint.
 
 - `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat`:
-  if `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of
+  if `A` and `B` are linearly disjoint, and if one of `A` and `B` is flat, then for any family of
   `R`-linearly independent elements `{ a_i }` of `A`, and any family of
   `R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is
   also `R`-linearly independent.