chore(LinearAlgebra/Matrix/Charpoly): place more decls in Matrix name…

…space (#10488)

Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

@@ -33,39 +33,40 @@ noncomputable section
 
 universe u v w
 
-open Polynomial Matrix BigOperators Polynomial
+namespace Matrix
+
+open BigOperators Finset Matrix Polynomial
 
 variable {R S : Type*} [CommRing R] [CommRing S]
 variable {m n : Type*} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n]
 variable (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₁ : Matrix n m R) (M₂₂ M : Matrix n n R)
 variable (i j : n)
 
-open Finset
 
 /-- The "characteristic matrix" of `M : Matrix n n R` is the matrix of polynomials $t I - M$.
 The determinant of this matrix is the characteristic polynomial.
 -/
 def charmatrix (M : Matrix n n R) : Matrix n n R[X] :=
   Matrix.scalar n (X : R[X]) - (C : R →+* R[X]).mapMatrix M
-#align charmatrix charmatrix
+#align charmatrix Matrix.charmatrix
 
 theorem charmatrix_apply :
     charmatrix M i j = (Matrix.diagonal fun _ : n => X) i j - C (M i j) :=
   rfl
-#align charmatrix_apply charmatrix_apply
+#align charmatrix_apply Matrix.charmatrix_apply
 
 @[simp]
 theorem charmatrix_apply_eq : charmatrix M i i = (X : R[X]) - C (M i i) := by
   simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, map_apply,
     diagonal_apply_eq]
 
-#align charmatrix_apply_eq charmatrix_apply_eq
+#align charmatrix_apply_eq Matrix.charmatrix_apply_eq
 
 @[simp]
 theorem charmatrix_apply_ne (h : i ≠ j) : charmatrix M i j = -C (M i j) := by
   simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, diagonal_apply_ne _ h,
     map_apply, sub_eq_neg_self]
-#align charmatrix_apply_ne charmatrix_apply_ne
+#align charmatrix_apply_ne Matrix.charmatrix_apply_ne
 
 theorem matPolyEquiv_charmatrix : matPolyEquiv (charmatrix M) = X - C M := by
   ext k i j
@@ -77,14 +78,14 @@ theorem matPolyEquiv_charmatrix : matPolyEquiv (charmatrix M) = X - C M := by
     split_ifs <;> simp
   · rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
     split_ifs <;> simp [h]
-#align mat_poly_equiv_charmatrix matPolyEquiv_charmatrix
+#align mat_poly_equiv_charmatrix Matrix.matPolyEquiv_charmatrix
 
 theorem charmatrix_reindex (e : n ≃ m) :
     charmatrix (reindex e e M) = reindex e e (charmatrix M) := by
   ext i j x
   by_cases h : i = j
   all_goals simp [h]
-#align charmatrix_reindex charmatrix_reindex
+#align charmatrix_reindex Matrix.charmatrix_reindex
 
 lemma charmatrix_map (M : Matrix n n R) (f : R →+* S) :
     charmatrix (M.map f) = (charmatrix M).map (Polynomial.map f) := by
@@ -97,8 +98,6 @@ lemma charmatrix_fromBlocks :
   simp only [charmatrix]
   ext (i|i) (j|j) : 2 <;> simp [diagonal]
 
-namespace Matrix
-
 /-- The characteristic polynomial of a matrix `M` is given by $\det (t I - M)$.
 -/
 def charpoly (M : Matrix n n R) : R[X] :=

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -37,29 +37,24 @@ noncomputable section
 
 universe u v w z
 
-open Polynomial Matrix BigOperators
+open BigOperators Finset Matrix Polynomial
 
 variable {R : Type u} [CommRing R]
-
 variable {n G : Type v} [DecidableEq n] [Fintype n]
-
 variable {α β : Type v} [DecidableEq α]
-
-open Finset
-
 variable {M : Matrix n n R}
 
+namespace Matrix
+
 theorem charmatrix_apply_natDegree [Nontrivial R] (i j : n) :
     (charmatrix M i j).natDegree = ite (i = j) 1 0 := by
   by_cases h : i = j <;> simp [h, ← degree_eq_iff_natDegree_eq_of_pos (Nat.succ_pos 0)]
-#align charmatrix_apply_nat_degree charmatrix_apply_natDegree
+#align charmatrix_apply_nat_degree Matrix.charmatrix_apply_natDegree
 
 theorem charmatrix_apply_natDegree_le (i j : n) :
     (charmatrix M i j).natDegree ≤ ite (i = j) 1 0 := by
   split_ifs with h <;> simp [h, natDegree_X_le]
-#align charmatrix_apply_nat_degree_le charmatrix_apply_natDegree_le
-
-namespace Matrix
+#align charmatrix_apply_nat_degree_le Matrix.charmatrix_apply_natDegree_le
 
 variable (M)
 
@@ -262,7 +257,7 @@ end Matrix
 
 variable {p : ℕ} [Fact p.Prime]
 
-theorem matPolyEquiv_eq_x_pow_sub_c {K : Type*} (k : ℕ) [Field K] (M : Matrix n n K) :
+theorem matPolyEquiv_eq_X_pow_sub_C {K : Type*} (k : ℕ) [Field K] (M : Matrix n n K) :
     matPolyEquiv ((expand K k : K[X] →+* K[X]).mapMatrix (charmatrix (M ^ k))) =
       X ^ k - C (M ^ k) := by
   -- porting note: `i` and `j` are used later on, but were not mentioned in mathlib3
@@ -280,7 +275,7 @@ theorem matPolyEquiv_eq_x_pow_sub_c {K : Type*} (k : ℕ) [Field K] (M : Matrix
       simp only [hij, zero_sub, Matrix.zero_apply, sub_zero, neg_zero, Matrix.one_apply_ne, Ne.def,
         not_false_iff]
 set_option linter.uppercaseLean3 false in
-#align mat_poly_equiv_eq_X_pow_sub_C matPolyEquiv_eq_x_pow_sub_c
+#align mat_poly_equiv_eq_X_pow_sub_C matPolyEquiv_eq_X_pow_sub_C
 
 namespace Matrix
 
@@ -298,8 +293,6 @@ theorem pow_eq_aeval_mod_charpoly (M : Matrix n n R) (k : ℕ) :
     M ^ k = aeval M (X ^ k %ₘ M.charpoly) := by rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
 #align matrix.pow_eq_aeval_mod_charpoly Matrix.pow_eq_aeval_mod_charpoly
 
-end Matrix
-
 section Ideal
 
 theorem coeff_charpoly_mem_ideal_pow {I : Ideal R} (h : ∀ i j, M i j ∈ I) (k : ℕ) :
@@ -320,12 +313,10 @@ theorem coeff_charpoly_mem_ideal_pow {I : Ideal R} (h : ∀ i j, M i j ∈ I) (k
     exact h (c i) i
   · rw [Nat.succ_eq_one_add, tsub_self_add, pow_zero, Ideal.one_eq_top]
     exact Submodule.mem_top
-#align coeff_charpoly_mem_ideal_pow coeff_charpoly_mem_ideal_pow
+#align coeff_charpoly_mem_ideal_pow Matrix.coeff_charpoly_mem_ideal_pow
 
 end Ideal
 
-namespace Matrix
-
 section reverse
 
 open Polynomial

Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

@@ -38,7 +38,7 @@ theorem FiniteField.Matrix.charpoly_pow_card {K : Type*} [Field K] [Fintype K] (
     apply congr_arg det
     refine' matPolyEquiv.injective _
     rw [AlgEquiv.map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
-    · exact (id (matPolyEquiv_eq_x_pow_sub_c (p ^ k) M) : _)
+    · exact (id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) : _)
     · exact (C M).commute_X
   · exact congr_arg _ (Subsingleton.elim _ _)
 #align finite_field.matrix.charpoly_pow_card FiniteField.Matrix.charpoly_pow_card