chore(linear_algebra/*): split lines and doc `direct_sum/tensor_produ…

…ct` (#6360)

This PR provides a short module doc to `direct_sum/tensor_product` (the file contains only one result). Furthermore, it splits lines in the `linear_algebra` folder. 



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

src/linear_algebra/basis.lean

@@ -91,7 +91,8 @@ lemma is_basis.injective [nontrivial R] (hv : is_basis R v) : injective v :=
   λ x y h, linear_independent.injective hv.1 h
 
 lemma is_basis.range (hv : is_basis R v) : is_basis R (λ x, x : range v → M) :=
-⟨hv.1.to_subtype_range, by { convert hv.2, ext i, exact ⟨λ ⟨p, hp⟩, hp ▸ p.2, λ hi, ⟨⟨i, hi⟩, rfl⟩⟩ }⟩
+⟨hv.1.to_subtype_range,
+  by { convert hv.2, ext i, exact ⟨λ ⟨p, hp⟩, hp ▸ p.2, λ hi, ⟨⟨i, hi⟩, rfl⟩⟩ }⟩
 
 /-- Given a basis, any vector can be written as a linear combination of the basis vectors. They are
 given by this linear map. This is one direction of `module_equiv_finsupp`. -/
@@ -289,11 +290,13 @@ begin
 end
 
 lemma linear_equiv_of_is_basis_trans_symm (e : ι ≃ ι') {v' : ι' → M'} (hv' : is_basis R v') :
-  (linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv e.symm) = linear_equiv.refl R M :=
+  (linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv e.symm) =
+  linear_equiv.refl R M :=
 by simp
 
 lemma linear_equiv_of_is_basis_symm_trans (e : ι ≃ ι') {v' : ι' → M'} (hv' : is_basis R v') :
-  (linear_equiv_of_is_basis hv' hv e.symm).trans (linear_equiv_of_is_basis hv hv' e) = linear_equiv.refl R M' :=
+  (linear_equiv_of_is_basis hv' hv e.symm).trans (linear_equiv_of_is_basis hv hv' e) =
+  linear_equiv.refl R M' :=
 by simp
 
 lemma is_basis_inl_union_inr {v : ι → M} {v' : ι' → M'}

src/linear_algebra/char_poly/coeff.lean

@@ -21,10 +21,10 @@ We give methods for computing coefficients of the characteristic polynomial.
 
 - `char_poly_degree_eq_dim` proves that the degree of the characteristic polynomial
   over a nonzero ring is the dimension of the matrix
-- `det_eq_sign_char_poly_coeff` proves that the determinant is the constant term of the characteristic
-  polynomial, up to sign.
-- `trace_eq_neg_char_poly_coeff` proves that the trace is the negative of the (d-1)th coefficient of the
-  characteristic polynomial, where d is the dimension of the matrix.
+- `det_eq_sign_char_poly_coeff` proves that the determinant is the constant term of the
+  characteristic polynomial, up to sign.
+- `trace_eq_neg_char_poly_coeff` proves that the trace is the negative of the (d-1)th coefficient of
+  the characteristic polynomial, where d is the dimension of the matrix.
   For a nonzero ring, this is the second-highest coefficient.
 
 -/
@@ -187,8 +187,8 @@ end
   char_poly (M ^ p) = char_poly M :=
 by { have h := finite_field.char_poly_pow_card M, rwa zmod.card at h, }
 
-lemma finite_field.trace_pow_card {K : Type*} [field K] [fintype K] [nonempty n] (M : matrix n n K) :
-  trace n K K (M ^ (fintype.card K)) = (trace n K K M) ^ (fintype.card K) :=
+lemma finite_field.trace_pow_card {K : Type*} [field K] [fintype K] [nonempty n]
+  (M : matrix n n K) : trace n K K (M ^ (fintype.card K)) = (trace n K K M) ^ (fintype.card K) :=
 by rw [trace_eq_neg_char_poly_coeff, trace_eq_neg_char_poly_coeff,
        finite_field.char_poly_pow_card, finite_field.pow_card]
 

src/linear_algebra/determinant.lean

@@ -254,7 +254,8 @@ lemma det_update_column_smul (M : matrix n n R) (j : n) (s : R) (u : n → R) :
   det (update_column M j $ s • u) = s * det (update_column M j u) :=
 begin
   simp only [det],
-  have : ∀ σ : perm n, ∏ i, M.update_column j (s • u) (σ i) i = s * ∏ i, M.update_column j u (σ i) i,
+  have : ∀ σ : perm n, ∏ i, M.update_column j (s • u) (σ i) i =
+    s * ∏ i, M.update_column j u (σ i) i,
   { intros σ,
     simp only [update_column_apply, prod_ite, filter_eq', finset.prod_singleton, finset.mem_univ,
                if_true, algebra.id.smul_eq_mul, pi.smul_apply],

src/linear_algebra/direct_sum/finsupp.lean

@@ -21,7 +21,8 @@ noncomputable theory
 open_locale classical direct_sum
 
 open set linear_map submodule
-variables {R : Type u} {M : Type v} {N : Type w} [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+variables {R : Type u} {M : Type v} {N : Type w} [ring R] [add_comm_group M] [module R M]
+  [add_comm_group N] [module R N]
 
 section finsupp_lequiv_direct_sum
 

src/linear_algebra/direct_sum/tensor_product.lean

@@ -3,9 +3,16 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro
 -/
+
 import linear_algebra.tensor_product
 import linear_algebra.direct_sum_module
 
+/-!
+# Tensor products of direct sums
+
+This file shows that taking `tensor_product`s commutes with taking `direct_sum`s in both arguments.
+-/
+
 section ring
 
 namespace tensor_product

src/linear_algebra/matrix.lean

@@ -473,7 +473,8 @@ lemma is_basis.iff_det {v : ι → M} : is_basis R v ↔ is_unit (he.det v) :=
 begin
   split,
   { intro hv,
-    suffices : is_unit (linear_map.to_matrix he he (linear_equiv_of_is_basis he hv $ equiv.refl ι)).det,
+    suffices :
+      is_unit (linear_map.to_matrix he he (linear_equiv_of_is_basis he hv $ equiv.refl ι)).det,
     { rw [is_basis.det_apply, is_basis.to_matrix_eq_to_matrix_constr],
       exact this },
     apply linear_equiv.is_unit_det },
@@ -748,7 +749,8 @@ reindex_refl_refl A
 
 lemma reindex_mul [semiring R]
   (eₘ : m ≃ m') (eₙ : n ≃ n') (eₗ : l ≃ l') (M : matrix m n R) (N : matrix n l R) :
-  (reindex_linear_equiv eₘ eₙ M) ⬝ (reindex_linear_equiv eₙ eₗ N) = reindex_linear_equiv eₘ eₗ (M ⬝ N) :=
+  (reindex_linear_equiv eₘ eₙ M) ⬝ (reindex_linear_equiv eₙ eₗ N) =
+  reindex_linear_equiv eₘ eₗ (M ⬝ N) :=
 begin
   ext i j,
   dsimp only [matrix.mul, matrix.dot_product],
@@ -761,7 +763,8 @@ types is an equivalence of algebras. -/
 def reindex_alg_equiv [comm_semiring R] [decidable_eq m] [decidable_eq n]
   (e : m ≃ n) : matrix m m R ≃ₐ[R] matrix n n R :=
 { map_mul'  := λ M N, by simp only [reindex_mul, linear_equiv.to_fun_apply, mul_eq_mul],
-  commutes' := λ r, by { ext, simp [algebra_map, algebra.to_ring_hom], by_cases h : i = j; simp [h], },
+  commutes' := λ r,
+                 by { ext, simp [algebra_map, algebra.to_ring_hom], by_cases h : i = j; simp [h], },
 ..(reindex_linear_equiv e e) }
 
 @[simp] lemma coe_reindex_alg_equiv [comm_semiring R] [decidable_eq m] [decidable_eq n]
@@ -916,9 +919,9 @@ if H : ∃ s : finset M, is_basis R (λ x, x : (↑s : set M) → M)
 then trace_aux R (classical.some_spec H)
 else 0
 
-theorem trace_eq_matrix_trace (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
-  {ι : Type w} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b) (f : M →ₗ[R] M) :
-  trace R M f = matrix.trace ι R R (linear_map.to_matrix hb hb f) :=
+theorem trace_eq_matrix_trace (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M]
+  [module R M] {ι : Type w} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b)
+  (f : M →ₗ[R] M) : trace R M f = matrix.trace ι R R (linear_map.to_matrix hb hb f) :=
 have ∃ s : finset M, is_basis R (λ x, x : (↑s : set M) → M),
 from ⟨finset.univ.image b,
   by { rw [finset.coe_image, finset.coe_univ, set.image_univ], exact hb.range }⟩,

src/linear_algebra/special_linear_group.lean

@@ -50,7 +50,8 @@ section
 
 variables (n : Type u) [decidable_eq n] [fintype n] (R : Type v) [comm_ring R]
 
-/-- `special_linear_group n R` is the group of `n` by `n` `R`-matrices with determinant equal to 1. -/
+/-- `special_linear_group n R` is the group of `n` by `n` `R`-matrices with determinant equal to 1.
+-/
 def special_linear_group := { A : matrix n n R // A.det = 1 }
 
 end