chore(group_theory/perm, linear_algebra/alternating): add some helper…

… lemmas for gh-5269 (#6186)

src/group_theory/perm/subgroup.lean

@@ -12,31 +12,50 @@ import group_theory.subgroup
 This file provides extra lemmas about some `subgroup`s that exist within `equiv.perm α`.
 `group_theory.subgroup` depends on `group_theory.perm.basic`, so these need to be in a separate
 file.
+
+It also provides decidable instances on membership in these subgroups, since
+`monoid_hom.decidable_mem_range` cannot be inferred without the help of a lambda.
+The presence of these instances induces a `fintype` instance on the `quotient_group.quotient` of
+these subgroups.
 -/
 
 namespace equiv
 namespace perm
 
 universes u
 
+instance sum_congr_hom.decidable_mem_range {α β : Type*}
+  [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
+  decidable_pred (λ x, x ∈ (sum_congr_hom α β).range) :=
+λ x, infer_instance
+
 @[simp]
 lemma sum_congr_hom.card_range {α β : Type*}
   [fintype (sum_congr_hom α β).range] [fintype (perm α × perm β)] :
   fintype.card (sum_congr_hom α β).range = fintype.card (perm α × perm β) :=
 fintype.card_eq.mpr ⟨(set.range (sum_congr_hom α β) sum_congr_hom_injective).symm⟩
 
+instance sigma_congr_right_hom.decidable_mem_range {α : Type*} {β : α → Type*}
+  [decidable_eq α] [∀ a, decidable_eq (β a)] [fintype α] [∀ a, fintype (β a)] :
+  decidable_pred (λ x, x ∈ (sigma_congr_right_hom β).range) :=
+λ x, infer_instance
+
 @[simp]
 lemma sigma_congr_right_hom.card_range {α : Type*} {β : α → Type*}
   [fintype (sigma_congr_right_hom β).range] [fintype (Π a, perm (β a))] :
   fintype.card (sigma_congr_right_hom β).range = fintype.card (Π a, perm (β a)) :=
 fintype.card_eq.mpr ⟨(set.range (sigma_congr_right_hom β) sigma_congr_right_hom_injective).symm⟩
 
+instance subtype_congr_hom.decidable_mem_range {α : Type*} (p : α → Prop) [decidable_pred p]
+  [fintype (perm {a // p a} × perm {a // ¬ p a})] [decidable_eq (perm α)] :
+  decidable_pred (λ x, x ∈ (subtype_congr_hom p).range) :=
+λ x, infer_instance
+
 @[simp]
 lemma subtype_congr_hom.card_range {α : Type*} (p : α → Prop) [decidable_pred p]
   [fintype (subtype_congr_hom p).range] [fintype (perm {a // p a} × perm {a // ¬ p a})] :
   fintype.card (subtype_congr_hom p).range = fintype.card (perm {a // p a} × perm {a // ¬ p a}) :=
 fintype.card_eq.mpr ⟨(set.range (subtype_congr_hom p) (subtype_congr_hom_injective p)).symm⟩
 
-
 end perm
 end equiv

src/linear_algebra/alternating.lean

@@ -400,6 +400,10 @@ lemma alternatization_def (m : multilinear_map R (λ i : ι, M) N') :
   ⇑(alternatization m) = (∑ (σ : perm ι), (σ.sign : ℤ) • m.dom_dom_congr σ : _) :=
 rfl
 
+lemma alternatization_coe (m : multilinear_map R (λ i : ι, M) N') :
+  ↑m.alternatization = (∑ (σ : perm ι), (σ.sign : ℤ) • m.dom_dom_congr σ : _) :=
+coe_inj rfl
+
 lemma alternatization_apply (m : multilinear_map R (λ i : ι, M) N') (v : ι → M) :
   alternatization m v = ∑ (σ : perm ι), (σ.sign : ℤ) • m.dom_dom_congr σ v :=
 by simp only [alternatization_def, smul_apply, sum_apply]