[Merged by Bors] - chore(*): swap order of [fintype A] [decidable_eq A]

src/algebra/lie_algebra.lean

@@ -788,7 +788,7 @@ section matrices
 open_locale matrix
 
 variables {R : Type u} [comm_ring R]
-variables {n : Type w} [fintype n] [decidable_eq n]
+variables {n : Type w} [decidable_eq n] [fintype n]
 
 /-- An important class of Lie rings are those arising from the associative algebra structure on
 square matrices over a commutative ring. -/
@@ -837,18 +837,18 @@ by simp [linear_equiv.symm_conj_apply, matrix.lie_conj, matrix.comp_to_matrix_mu
 
 /-- For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent
 types is an equivalence of Lie algebras. -/
-def matrix.reindex_lie_equiv {m : Type w₁} [fintype m] [decidable_eq m]
+def matrix.reindex_lie_equiv {m : Type w₁} [decidable_eq m] [fintype m]
   (e : n ≃ m) : matrix n n R ≃ₗ⁅R⁆ matrix m m R :=
 { map_lie := λ M N, by simp only [lie_ring.of_associative_ring_bracket, matrix.reindex_mul,
     matrix.mul_eq_mul, linear_equiv.map_sub, linear_equiv.to_fun_apply],
 ..(matrix.reindex_linear_equiv e e) }
 
-@[simp] lemma matrix.reindex_lie_equiv_apply {m : Type w₁} [fintype m] [decidable_eq m]
+@[simp] lemma matrix.reindex_lie_equiv_apply {m : Type w₁} [decidable_eq m] [fintype m]
   (e : n ≃ m) (M : matrix n n R) :
   matrix.reindex_lie_equiv e M = λ i j, M (e.symm i) (e.symm j) :=
 rfl
 
-@[simp] lemma matrix.reindex_lie_equiv_symm_apply {m : Type w₁} [fintype m] [decidable_eq m]
+@[simp] lemma matrix.reindex_lie_equiv_symm_apply {m : Type w₁} [decidable_eq m] [fintype m]
   (e : n ≃ m) (M : matrix m m R) :
   (matrix.reindex_lie_equiv e).symm M = λ i j, M (e i) (e j) :=
 rfl
@@ -905,7 +905,7 @@ end skew_adjoint_endomorphisms
 section skew_adjoint_matrices
 open_locale matrix
 
-variables {R : Type u} {n : Type w} [comm_ring R] [fintype n] [decidable_eq n]
+variables {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n]
 variables (J : matrix n n R)
 
 local attribute [instance] matrix.lie_ring
@@ -955,7 +955,7 @@ by simp [skew_adjoint_matrices_lie_subalgebra_equiv]
 
 /-- An equivalence of matrix algebras commuting with the transpose endomorphisms restricts to an
 equivalence of Lie algebras of skew-adjoint matrices. -/
-def skew_adjoint_matrices_lie_subalgebra_equiv_transpose {m : Type w} [fintype m] [decidable_eq m]
+def skew_adjoint_matrices_lie_subalgebra_equiv_transpose {m : Type w} [decidable_eq m] [fintype m]
   (e : matrix n n R ≃ₐ[R] matrix m m R) (h : ∀ A, (e A)ᵀ = e (Aᵀ)) :
   skew_adjoint_matrices_lie_subalgebra J ≃ₗ⁅R⁆ skew_adjoint_matrices_lie_subalgebra (e J) :=
 lie_algebra.equiv.of_subalgebras _ _ e.to_lie_equiv
@@ -967,7 +967,7 @@ begin
 end
 
 @[simp] lemma skew_adjoint_matrices_lie_subalgebra_equiv_transpose_apply
-  {m : Type w} [fintype m] [decidable_eq m]
+  {m : Type w} [decidable_eq m] [fintype m]
   (e : matrix n n R ≃ₐ[R] matrix m m R) (h : ∀ A, (e A)ᵀ = e (Aᵀ))
   (A : skew_adjoint_matrices_lie_subalgebra J) :
   (skew_adjoint_matrices_lie_subalgebra_equiv_transpose J e h A : matrix m m R) = e A :=

src/data/equiv/list.lean

@@ -105,13 +105,13 @@ by haveI := decidable_eq_of_encodable α; exact
  of_equiv {s : multiset α // s.nodup}
   ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ⟨a, b⟩, rfl⟩
 
-def fintype_arrow (α : Type*) (β : Type*) [fintype α] [decidable_eq α] [encodable β] :
+def fintype_arrow (α : Type*) (β : Type*) [decidable_eq α] [fintype α] [encodable β] :
   trunc (encodable (α → β)) :=
 (fintype.equiv_fin α).map $
   λf, encodable.of_equiv (fin (fintype.card α) → β) $
   equiv.arrow_congr f (equiv.refl _)
 
-def fintype_pi (α : Type*) (π : α → Type*) [fintype α] [decidable_eq α] [∀a, encodable (π a)] :
+def fintype_pi (α : Type*) (π : α → Type*) [decidable_eq α] [fintype α] [∀a, encodable (π a)] :
   trunc (encodable (Πa, π a)) :=
 (encodable.trunc_encodable_of_fintype α).bind $ λa,
   (@fintype_arrow α (Σa, π a) _ _ (@encodable.sigma _ _ a _)).bind $ λf,

src/data/fintype/basic.lean

@@ -144,7 +144,7 @@ def equiv_fin_of_forall_mem_list {α} [decidable_eq α]
   `n = card α`. Since it is not unique, and depends on which permutation
   of the universe list is used, the bijection is wrapped in `trunc` to
   preserve computability.  -/
-def equiv_fin (α) [fintype α] [decidable_eq α] : trunc (α ≃ fin (card α)) :=
+def equiv_fin (α) [decidable_eq α] [fintype α] : trunc (α ≃ fin (card α)) :=
 by unfold card finset.card; exact
 quot.rec_on_subsingleton (@univ α _).1
   (λ l (h : ∀ x:α, x ∈ l) (nd : l.nodup), trunc.mk (equiv_fin_of_forall_mem_list h nd))
@@ -190,7 +190,7 @@ def of_bijective [fintype α] (f : α → β) (H : function.bijective f) : finty
 λ b, let ⟨a, e⟩ := H.2 b in e ▸ mem_map_of_mem _ (mem_univ _)⟩
 
 /-- If `f : α → β` is a surjection and `α` is a fintype, then `β` is also a fintype. -/
-def of_surjective [fintype α] [decidable_eq β] (f : α → β) (H : function.surjective f) : fintype β :=
+def of_surjective [decidable_eq β] [fintype α] (f : α → β) (H : function.surjective f) : fintype β :=
 ⟨univ.image f, λ b, let ⟨a, e⟩ := H b in e ▸ mem_image_of_mem _ (mem_univ _)⟩
 
 noncomputable def of_injective [fintype β] (f : α → β) (H : function.injective f) : fintype α :=
@@ -258,7 +258,7 @@ end set
 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=
 rfl
 
-lemma finset.card_univ_diff [fintype α] [decidable_eq α] (s : finset α) :
+lemma finset.card_univ_diff [decidable_eq α] [fintype α] (s : finset α) :
   (finset.univ \ s).card = fintype.card α - s.card :=
 finset.card_sdiff (subset_univ s)
 
@@ -572,7 +572,7 @@ by rw [← e.equiv_of_fintype_self_embedding_to_embedding, univ_map_equiv_to_emb
 
 namespace fintype
 
-variables [fintype α] [decidable_eq α] {δ : α → Type*}
+variables [decidable_eq α] [fintype α] {δ : α → Type*}
 
 /-- Given for all `a : α` a finset `t a` of `δ a`, then one can define the
 finset `fintype.pi_finset t` of all functions taking values in `t a` for all `a`. This is the
@@ -732,7 +732,7 @@ theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
   subst j, refl
 end
 
-def quotient.fin_choice {ι : Type*} [fintype ι] [decidable_eq ι]
+def quotient.fin_choice {ι : Type*} [decidable_eq ι] [fintype ι]
   {α : ι → Type*} [S : ∀ i, setoid (α i)]
   (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
 quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
@@ -750,7 +750,7 @@ quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
   (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
   (λ a b h, quotient.sound $ λ i, h _ _)
 
-theorem quotient.fin_choice_eq {ι : Type*} [fintype ι] [decidable_eq ι]
+theorem quotient.fin_choice_eq {ι : Type*} [decidable_eq ι] [fintype ι]
   {α : ι → Type*} [∀ i, setoid (α i)]
   (f : ∀ i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
 begin
@@ -901,7 +901,7 @@ section choose
 open fintype
 open equiv
 
-variables [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p]
+variables [decidable_eq α] [fintype α] (p : α → Prop) [decidable_pred p]
 
 def choose_x (hp : ∃! a : α, p a) : {a // p a} :=
 ⟨finset.choose p univ (by simp; exact hp), finset.choose_property _ _ _⟩
@@ -916,8 +916,8 @@ end choose
 section bijection_inverse
 open function
 
-variables [fintype α] [decidable_eq α]
-variables [fintype β] [decidable_eq β]
+variables [decidable_eq α] [fintype α]
+variables [decidable_eq β] [fintype β]
 variables {f : α → β}
 
 /-- `

src/data/fintype/card.lean

@@ -30,7 +30,7 @@ finset.card_eq_sum_ones _
 section
 open finset
 
-variables {ι : Type*} [fintype ι] [decidable_eq ι]
+variables {ι : Type*} [decidable_eq ι] [fintype ι]
 
 @[to_additive]
 lemma prod_extend_by_one [comm_monoid α] (s : finset ι) (f : ι → α) :
@@ -120,12 +120,12 @@ multiset.card_pi _ _
   (fintype.pi_finset t).card = ∏ a, card (t a) :=
 by simp [fintype.pi_finset, card_map]
 
-@[simp] lemma fintype.card_pi {β : α → Type*} [fintype α] [decidable_eq α]
+@[simp] lemma fintype.card_pi {β : α → Type*} [decidable_eq α] [fintype α]
   [f : Π a, fintype (β a)] : fintype.card (Π a, β a) = ∏ a, fintype.card (β a) :=
 fintype.card_pi_finset _
 
 -- FIXME ouch, this should be in the main file.
-@[simp] lemma fintype.card_fun [fintype α] [decidable_eq α] [fintype β] :
+@[simp] lemma fintype.card_fun [decidable_eq α] [fintype α] [fintype β] :
   fintype.card (α → β) = fintype.card β ^ fintype.card α :=
 by rw [fintype.card_pi, finset.prod_const, nat.pow_eq_pow]; refl
 
@@ -229,7 +229,7 @@ begin
   simp [finset.ext_iff]
 end
 
-@[to_additive] lemma finset.prod_fiberwise [fintype β] [decidable_eq β] [comm_monoid γ]
+@[to_additive] lemma finset.prod_fiberwise [decidable_eq β] [fintype β] [comm_monoid γ]
   (s : finset α) (f : α → β) (g : α → γ) :
   ∏ b : β, ∏ a in s.filter (λ a, f a = b), g a = ∏ a in s, g a :=
 begin
@@ -247,7 +247,7 @@ begin
 end
 
 @[to_additive]
-lemma fintype.prod_fiberwise [fintype α] [fintype β] [decidable_eq β] [comm_monoid γ]
+lemma fintype.prod_fiberwise [fintype α] [decidable_eq β] [fintype β] [comm_monoid γ]
   (f : α → β) (g : α → γ) :
   (∏ b : β, ∏ a : {a // f a = b}, g (a : α)) = ∏ a, g a :=
 begin

src/data/matrix/basic.lean

@@ -425,7 +425,7 @@ end
 The ring homomorphism `α →+* matrix n n α`
 sending `a` to the diagonal matrix with `a` on the diagonal.
 -/
-def scalar (n : Type u) [fintype n] [decidable_eq n] : α →+* matrix n n α :=
+def scalar (n : Type u) [decidable_eq n] [fintype n] : α →+* matrix n n α :=
 { to_fun := λ a, a • 1,
   map_zero' := by simp,
   map_add' := by { intros, ext, simp [add_mul], },

src/field_theory/finite.lean

@@ -49,7 +49,7 @@ open polynomial
 
 /-- The cardinality of a field is at most `n` times the cardinality of the image of a degree `n`
   polynomial -/
-lemma card_image_polynomial_eval [fintype R] [decidable_eq R] {p : polynomial R} (hp : 0 < p.degree) :
+lemma card_image_polynomial_eval [decidable_eq R] [fintype R] {p : polynomial R} (hp : 0 < p.degree) :
   fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
 finset.card_le_mul_card_image _ _
   (λ a _, calc _ = (p - C a).roots.card : congr_arg card

src/group_theory/order_of_element.lean

@@ -304,13 +304,13 @@ def is_cyclic.comm_group [hg : group α] [is_cyclic α] : comm_group α :=
     hm ▸ hn ▸ gpow_mul_comm _ _ _,
   ..hg }
 
-lemma is_cyclic_of_order_of_eq_card [group α] [fintype α] [decidable_eq α]
+lemma is_cyclic_of_order_of_eq_card [group α] [decidable_eq α] [fintype α]
   (x : α) (hx : order_of x = fintype.card α) : is_cyclic α :=
 ⟨⟨x, set.eq_univ_iff_forall.1 $ set.eq_of_subset_of_card_le
   (set.subset_univ _)
   (by {rw [fintype.card_congr (equiv.set.univ α), ← hx, order_eq_card_gpowers], refl})⟩⟩
 
-lemma order_of_eq_card_of_forall_mem_gpowers [group α] [fintype α] [decidable_eq α]
+lemma order_of_eq_card_of_forall_mem_gpowers [group α] [decidable_eq α] [fintype α]
   {g : α} (hx : ∀ x, x ∈ gpowers g) : order_of g = fintype.card α :=
 by {rw [← fintype.card_congr (equiv.set.univ α), order_eq_card_gpowers],
   simp [hx], apply fintype.card_of_finset', simp, intro x, exact hx x}
@@ -362,7 +362,7 @@ else
   by clear _let_match; substI this; apply_instance
 
 open finset nat
-lemma is_cyclic.card_pow_eq_one_le [group α] [fintype α] [decidable_eq α] [is_cyclic α] {n : ℕ}
+lemma is_cyclic.card_pow_eq_one_le [group α] [decidable_eq α] [fintype α] [is_cyclic α] {n : ℕ}
   (hn0 : 0 < n) : (univ.filter (λ a : α, a ^ n = 1)).card ≤ n :=
 let ⟨g, hg⟩ := is_cyclic.exists_generator α in
 calc (univ.filter (λ a : α, a ^ n = 1)).card
@@ -397,7 +397,7 @@ by { simp only [mem_powers_iff_mem_gpowers], exact is_cyclic.exists_generator α
 
 section
 
-variables [group α] [fintype α] [decidable_eq α]
+variables [group α] [decidable_eq α] [fintype α]
 
 lemma is_cyclic.image_range_order_of (ha : ∀ x : α, x ∈ gpowers a) :
   finset.image (λ i, a ^ i) (range (order_of a)) = univ :=
@@ -415,7 +415,7 @@ end
 
 section totient
 
-variables [group α] [fintype α] [decidable_eq α] (hn : ∀ n : ℕ, 0 < n → (univ.filter (λ a : α, a ^ n = 1)).card ≤ n)
+variables [group α] [decidable_eq α] [fintype α] (hn : ∀ n : ℕ, 0 < n → (univ.filter (λ a : α, a ^ n = 1)).card ≤ n)
 include hn
 
 lemma card_pow_eq_one_eq_order_of_aux (a : α) :
@@ -515,7 +515,7 @@ is_cyclic_of_order_of_eq_card x (finset.mem_filter.1 hx).2
 
 end totient
 
-lemma is_cyclic.card_order_of_eq_totient [group α] [is_cyclic α] [fintype α] [decidable_eq α]
+lemma is_cyclic.card_order_of_eq_totient [group α] [is_cyclic α] [decidable_eq α] [fintype α]
   {d : ℕ} (hd : d ∣ fintype.card α) : (univ.filter (λ a : α, order_of a = d)).card = totient d :=
 card_order_of_eq_totient_aux₂ (λ n, is_cyclic.card_pow_eq_one_le) hd
 

src/linear_algebra/char_poly.lean

@@ -32,7 +32,7 @@ open polynomial matrix
 open_locale big_operators
 
 variables {R : Type u} [comm_ring R]
-variables {n : Type w} [fintype n] [decidable_eq n]
+variables {n : Type w} [decidable_eq n] [fintype n]
 
 open finset
 

src/linear_algebra/char_poly/coeff.lean

@@ -35,7 +35,7 @@ open polynomial matrix
 open_locale big_operators
 
 variables {R : Type u} [comm_ring R]
-variables {n G : Type v} [fintype n] [decidable_eq n]
+variables {n G : Type v} [decidable_eq n] [fintype n]
 variables {α β : Type v} [decidable_eq α]
 
 

src/linear_algebra/determinant.lean

@@ -14,7 +14,7 @@ open equiv equiv.perm finset function
 namespace matrix
 open_locale matrix big_operators
 
-variables {n : Type u} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R]
+variables {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R]
 
 local notation `ε` σ:max := ((sign σ : ℤ ) : R)
 

src/linear_algebra/matrix.lean

@@ -125,7 +125,7 @@ def to_matrix [decidable_eq n] : ((n → R) →ₗ[R] (m → R)) → matrix m n
   (@linear_map.id _ (n → R) _ _ _).to_matrix = 1 :=
 by { ext, simp [to_matrix, to_matrixₗ, matrix.one_apply, eq_comm] }
 
-theorem to_matrix_of_equiv {p q : Type*} [fintype p] [fintype q] [decidable_eq n] [decidable_eq q]
+theorem to_matrix_of_equiv {p q : Type*} [decidable_eq n] [decidable_eq q] [fintype p] [fintype q]
   (e₁ : m ≃ p) (e₂ : n ≃ q) (f : (q → R) →ₗ[R] (p → R)) (i j) :
   to_matrix f (e₁ i) (e₂ j) = to_matrix (linear_equiv.arrow_congr
       (linear_map.fun_congr_left R R e₂)
@@ -197,7 +197,7 @@ between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases. -
 def linear_equiv_matrix {ι κ M₁ M₂ : Type*}
   [add_comm_group M₁] [module R M₁]
   [add_comm_group M₂] [module R M₂]
-  [fintype ι] [decidable_eq ι] [fintype κ]
+  [decidable_eq ι] [fintype ι] [fintype κ]
   {v₁ : ι → M₁} {v₂ : κ → M₂} (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) :
   (M₁ →ₗ[R] M₂) ≃ₗ[R] matrix κ ι R :=
 linear_equiv.trans (linear_equiv.arrow_congr (equiv_fun_basis hv₁) (equiv_fun_basis hv₂)) linear_equiv_matrix'
@@ -241,7 +241,7 @@ lemma linear_equiv_matrix_comp {R ι κ μ M₁ M₂ M₃ : Type*} [comm_ring R]
   [add_comm_group M₁] [module R M₁]
   [add_comm_group M₂] [module R M₂]
   [add_comm_group M₃] [module R M₃]
-  [fintype ι] [decidable_eq ι] [fintype κ] [decidable_eq κ] [fintype μ]
+  [decidable_eq ι] [fintype ι] [decidable_eq κ] [fintype κ] [fintype μ]
   {v₁ : ι → M₁} {v₂ : κ → M₂} {v₃ : μ → M₃}
   (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) (hv₃ : is_basis R v₃)
   (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
@@ -251,7 +251,7 @@ by simp_rw [linear_equiv_matrix, linear_equiv.trans_apply, linear_equiv_matrix'_
     linear_equiv.arrow_congr_comp _ (equiv_fun_basis hv₂), comp_to_matrix_mul]
 
 lemma linear_equiv_matrix_mul {R M ι : Type*} [comm_ring R]
-  [add_comm_group M] [module R M] [fintype ι] [decidable_eq ι]
+  [add_comm_group M] [module R M] [decidable_eq ι] [fintype ι]
   {b : ι → M} (hb : is_basis R b) (f g : M →ₗ[R] M) :
   linear_equiv_matrix hb hb (f * g) = linear_equiv_matrix hb hb f * linear_equiv_matrix hb hb g :=
 linear_equiv_matrix_comp hb hb hb f g
@@ -499,18 +499,18 @@ open_locale matrix
 
 /-- The trace of an endomorphism given a basis. -/
 def trace_aux (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) :
+  {ι : Type w} [decidable_eq ι] [fintype ι] {b : ι → M} (hb : is_basis R b) :
   (M →ₗ[R] M) →ₗ[R] R :=
 (matrix.trace ι R R).comp $ linear_equiv_matrix hb hb
 
 @[simp] lemma trace_aux_def (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) :
+  {ι : Type w} [decidable_eq ι] [fintype ι] {b : ι → M} (hb : is_basis R b) (f : M →ₗ[R] M) :
   trace_aux R hb f = matrix.trace ι R R (linear_equiv_matrix hb hb f) :=
 rfl
 
 theorem trace_aux_eq' (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)
-  {κ : Type w} [fintype κ] [decidable_eq κ] {c : κ → M} (hc : is_basis R c) :
+  {ι : Type w} [decidable_eq ι] [fintype ι] {b : ι → M} (hb : is_basis R b)
+  {κ : Type w} [decidable_eq κ] [fintype κ] {c : κ → M} (hc : is_basis R c) :
   trace_aux R hb = trace_aux R hc :=
 linear_map.ext $ λ f,
 calc  matrix.trace ι R R (linear_equiv_matrix hb hb f)
@@ -544,8 +544,8 @@ end
 
 /-- where `ι` and `κ` can reside in different universes -/
 theorem trace_aux_eq (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
-  {ι : Type*} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b)
-  {κ : Type*} [fintype κ] [decidable_eq κ] {c : κ → M} (hc : is_basis R c) :
+  {ι : Type*} [decidable_eq ι] [fintype ι] {b : ι → M} (hb : is_basis R b)
+  {κ : Type*} [decidable_eq κ] [fintype κ] {c : κ → M} (hc : is_basis R c) :
   trace_aux R hb = trace_aux R hc :=
 calc  trace_aux R hb
     = trace_aux R hb.range : by { rw trace_aux_range R hb, congr }

src/linear_algebra/nonsingular_inverse.lean

@@ -45,7 +45,7 @@ matrix inverse, cramer, cramer's rule, adjugate
 
 namespace matrix
 universes u v
-variables {n : Type u} [fintype n] [decidable_eq n] {α : Type v}
+variables {n : Type u} [decidable_eq n] [fintype n] {α : Type v}
 open_locale matrix big_operators
 open equiv equiv.perm finset
 

src/linear_algebra/quadratic_form.lean

@@ -447,7 +447,7 @@ namespace quadratic_form
 
 variables {n : Type w} [fintype n]
 variables [decidable_eq n] [invertible (2 : R₁)]
-variables {m : Type w} [fintype m] [decidable_eq m]
+variables {m : Type w} [decidable_eq m] [fintype m]
 open_locale matrix
 
 @[simp]

src/linear_algebra/special_linear_group.lean

@@ -48,7 +48,7 @@ open linear_map
 
 section
 
-variables (n : Type u) [fintype n] [decidable_eq n] (R : Type v) [comm_ring R]
+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. -/
 def special_linear_group := { A : matrix n n R // A.det = 1 }
@@ -57,7 +57,7 @@ end
 
 namespace special_linear_group
 
-variables {n : Type u} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R]
+variables {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R]
 
 instance coe_matrix : has_coe (special_linear_group n R) (matrix n n R) :=
 ⟨λ A, A.val⟩