chore(linear_algebra/alternating): make ι an explicit arg of alternating_map.const_of_is_empty (#19123)

urkud · urkud · commit bd65478311e4 · 2023-05-30T03:49:43.000Z
While for general multilinear maps one can deduce it from the type of `E : ι -&gt; Type*`, this doesn't work for alternating maps.
diff --git a/src/analysis/inner_product_space/orientation.lean b/src/analysis/inner_product_space/orientation.lean
@@ -181,7 +181,7 @@ alternating form uniquely defined by compatibility with the orientation and inne
 begin
   classical,
   unfreezingI { cases n },
-  { let opos : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (1:ℝ),
+  { let opos : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (fin 0) (1:ℝ),
     exact o.eq_or_eq_neg_of_is_empty.by_cases (λ _, opos) (λ _, -opos) },
   { exact (o.fin_orthonormal_basis n.succ_pos _i.out).to_basis.det }
 end
diff --git a/src/linear_algebra/alternating.lean b/src/linear_algebra/alternating.lean
@@ -337,6 +337,8 @@ def of_subsingleton [subsingleton ι] (i : ι) : alternating_map R M M ι :=
   map_eq_zero_of_eq' := λ v i j hv hij, (hij $ subsingleton.elim _ _).elim,
   ..multilinear_map.of_subsingleton R M i }
 
+variable (ι)
+
 /-- The constant map is alternating when `ι` is empty. -/
 @[simps {fully_applied := ff}]
 def const_of_is_empty [is_empty ι] (m : N) : alternating_map R M N ι :=
@@ -1102,7 +1104,7 @@ end
 to an empty family. -/
 @[simps] def const_linear_equiv_of_is_empty [is_empty ι] :
   N'' ≃ₗ[R'] alternating_map R' M'' N'' ι :=
-{ to_fun    := alternating_map.const_of_is_empty R' M'',
+{ to_fun    := alternating_map.const_of_is_empty R' M'' ι,
   map_add'  := λ x y, rfl,
   map_smul' := λ t x, rfl,
   inv_fun   := λ f, f 0,
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
@@ -480,7 +480,7 @@ lemma basis.det_apply (v : ι → M) : e.det v = det (e.to_matrix v) := rfl
 lemma basis.det_self : e.det e = 1 :=
 by simp [e.det_apply]
 
-@[simp] lemma basis.det_is_empty [is_empty ι] : e.det = alternating_map.const_of_is_empty R M 1 :=
+@[simp] lemma basis.det_is_empty [is_empty ι] : e.det = alternating_map.const_of_is_empty R M ι 1 :=
 begin
   ext v,
   exact matrix.det_is_empty,
