feat: port GroupTheory.Perm.Sign (#2458)

Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
leanprover-community · Feb 27, 2023 · 82cc6f6 · 82cc6f6
1 parent 90a3158
commit 82cc6f6
Show file tree

Hide file tree

Showing 3 changed files with 828 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -787,6 +787,7 @@ import Mathlib.GroupTheory.NoncommPiCoprod
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.GroupTheory.Perm.Basic
 import Mathlib.GroupTheory.Perm.List
+import Mathlib.GroupTheory.Perm.Sign
 import Mathlib.GroupTheory.Perm.Subgroup
 import Mathlib.GroupTheory.Perm.Support
 import Mathlib.GroupTheory.Perm.ViaEmbedding

diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean
@@ -364,7 +364,7 @@ theorem subtypePerm_apply (f : Perm α) (h : ∀ x, p x ↔ p (f x)) (x : { x //
 
 @[simp]
 theorem subtypePerm_one (p : α → Prop) (h := fun _ => Iff.rfl) : @subtypePerm α p 1 h = 1 :=
-  Equiv.ext fun ⟨_, _⟩ => rfl
+  rfl
 #align equiv.perm.subtype_perm_one Equiv.Perm.subtypePerm_one
 
 @[simp]