chore(LinearAlgebra/{ExteriorAlgebra,ExteriorPower}): refactor ExteriorAlgebra.ιMulti_family and exteriorPower.ιMulti_family to use Set.powersetCard (#35167)

Rewrites `ExteriorAlgebra.ιMulti_family` and `exteriorPower.ιMulti_family` to use `Set.powersetCard` instead of an explicit subtype.

Author: morrison-daniel

Mathlib.lean

@@ -5658,6 +5658,7 @@ public import Mathlib.Order.Hom.CompleteLattice
 public import Mathlib.Order.Hom.Lattice
 public import Mathlib.Order.Hom.Lex
 public import Mathlib.Order.Hom.Order
+public import Mathlib.Order.Hom.PowersetCard
 public import Mathlib.Order.Hom.Set
 public import Mathlib.Order.Hom.WithTopBot
 public import Mathlib.Order.Ideal

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 public import Mathlib.LinearAlgebra.Alternating.Curry
+public import Mathlib.Order.Hom.PowersetCard
 
 /-!
 # Exterior Algebras
@@ -341,8 +342,8 @@ lemma ιMulti_span_fixedDegree (n : ℕ) :
 /-- Given a linearly ordered family `v` of vectors of `M` and a natural number `n`, produce the
 family of `n`fold exterior products of elements of `v`, seen as members of the exterior algebra. -/
 abbrev ιMulti_family (n : ℕ) {I : Type*} [LinearOrder I] (v : I → M)
-    (s : {s : Finset I // Finset.card s = n}) : ExteriorAlgebra R M :=
-  ιMulti R n fun i => v (Finset.orderIsoOfFin _ s.prop i)
+    (s : Set.powersetCard I n) : ExteriorAlgebra R M :=
+  ιMulti R n (v ∘ (Set.powersetCard.ofFinEmbEquiv.symm s))
 
 variable {R}
 

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

@@ -46,7 +46,7 @@ variable (R : Type u) [CommRing R] (n : ℕ) {M N N' : Type*}
 
 namespace exteriorPower
 
-open Function
+open Function Set Set.powersetCard
 
 /-! The canonical alternating map from `Fin n → M` to `⋀[R]^n M`. -/
 
@@ -63,15 +63,15 @@ def ιMulti : M [⋀^Fin n]→ₗ[R] (⋀[R]^n M) :=
 family of `n`fold exterior products of elements of `v`, seen as members of the
 `n`th exterior power. -/
 noncomputable def ιMulti_family {I : Type*} [LinearOrder I] (v : I → M)
-    (s : {s : Finset I // Finset.card s = n}) : ⋀[R]^n M :=
-  ιMulti R n fun i ↦ v <| Finset.orderIsoOfFin s.val s.property i
+    (s : powersetCard I n) : ⋀[R]^n M :=
+  ιMulti R n (v ∘ (ofFinEmbEquiv.symm s))
 
 lemma ιMulti_family_eq_coe_comp {I : Type*} [LinearOrder I] (v : I → M) :
     ExteriorAlgebra.ιMulti_family R n v = (↑) ∘ ιMulti_family R n v :=
   rfl
 
 @[simp] lemma ιMulti_family_apply_coe {I : Type*} [LinearOrder I] (v : I → M)
-    (s : {s : Finset I // Finset.card s = n}) :
+    (s : powersetCard I n) :
     ιMulti_family R n v s = ExteriorAlgebra.ιMulti_family R n v s := rfl
 
 variable (M)
@@ -281,7 +281,7 @@ lemma map_comp_ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (f : M 
 
 @[simp]
 lemma map_apply_ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N)
-    (s : {s : Finset I // s.card = n}) :
+    (s : powersetCard I n) :
     (map n f) (ιMulti_family R n v s) = ιMulti_family R n (f ∘ v) s := by
   simp only [ιMulti_family, map, alternatingMapLinearEquiv_apply_ιMulti]
   rfl

Mathlib/Order/Hom/PowersetCard.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2026 Daniel Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Morrison
+-/
+module
+
+public import Mathlib.Data.Set.PowersetCard
+public import Mathlib.Data.Finset.Sort
+
+@[expose] public section
+
+open Finset Function Set
+
+namespace Set.powersetCard
+
+section order
+
+variable {n : ℕ} {I : Type*} [LinearOrder I]
+
+/-- The isomorphism of `OrderEmbedding`s from `Fin n` into `I` with `Set.powersetCard I n`
+when `I` is linearly ordered. -/
+def ofFinEmbEquiv : (Fin n ↪o I) ≃ powersetCard I n where
+  toFun f := ofFinEmb n I f.toEmbedding
+  invFun s := Finset.orderEmbOfFin s.val s.prop
+  left_inv f := by symm; apply Finset.orderEmbOfFin_unique'; simp
+  right_inv s := by ext; simp
+
+lemma ofFinEmbEquiv_apply (f : Fin n ↪o I) :
+    ofFinEmbEquiv f = ofFinEmb n I f.toEmbedding :=
+  rfl
+
+lemma ofFinEmbEquiv_symm_apply (s : powersetCard I n) :
+    ofFinEmbEquiv.symm s = Finset.orderEmbOfFin s.val s.prop := rfl
+
+end order
+
+end Set.powersetCard