feat(linear_algebra/matrix/determinant): generalize det_fin_zero to d…

…et_eq_one_of_is_empty (#8387)

Also golfs a nearby proof

src/data/equiv/basic.lean

@@ -173,8 +173,8 @@ instance equiv_subsingleton_dom [subsingleton α] :
   subsingleton (α ≃ β) :=
 ⟨λ f g, equiv.ext $ λ x, @subsingleton.elim _ (equiv.subsingleton.symm f) _ _⟩
 
-instance perm_subsingleton [subsingleton α] : subsingleton (perm α) :=
-equiv.equiv_subsingleton_cod
+instance perm_unique [subsingleton α] : unique (perm α) :=
+{ default := equiv.refl α, uniq := λ _, subsingleton.elim _ _ }
 
 lemma perm.subsingleton_eq_refl [subsingleton α] (e : perm α) :
   e = equiv.refl α := subsingleton.elim _ _

src/data/fintype/basic.lean

@@ -529,8 +529,9 @@ subsingleton.elim (of_subsingleton $ default α) h ▸ card_of_subsingleton _
 instance of_is_empty [is_empty α] : fintype α := ⟨∅, is_empty_elim⟩
 
 /-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
-arbitrary `fintype` instances, use `fintype.univ_eq_empty'`. -/
-@[simp] theorem univ_of_is_empty [is_empty α] : @univ α _ = ∅ := rfl
+arbitrary `fintype` instances, use `fintype.univ_is_empty`. -/
+-- no-lint since while `fintype.of_is_empty` can prove this, it isn't applicable for `dsimp`.
+@[simp, nolint simp_nf] theorem univ_of_is_empty [is_empty α] : @univ α _ = ∅ := rfl
 
 /-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
 arbitrary `fintype` instances, use `fintype.card_eq_zero_iff`. -/
@@ -703,6 +704,9 @@ fintype.of_subsingleton (default α)
 @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
 by rw [subsingleton.elim f (@unique.fintype α _)]; refl
 
+@[simp] lemma univ_is_empty {α : Type*} [is_empty α] [fintype α] : @finset.univ α _ = ∅ :=
+finset.ext is_empty_elim
+
 @[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
 
 @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
@@ -876,6 +880,10 @@ lemma card_eq_zero_iff : card α = 0 ↔ is_empty α :=
 ⟨λ h, ⟨λ a, have e : α ≃ empty := classical.choice (card_eq.1 (by simp [h])), (e a).elim⟩,
   λ h, by { have e : α ≃ empty, exactI equiv.equiv_empty α, simp [card_congr e] }⟩
 
+lemma card_eq_one_iff_nonempty_unique : card α = 1 ↔ nonempty (unique α) :=
+⟨λ h, let ⟨d, h⟩ := fintype.card_eq_one_iff.mp h in ⟨{ default := d, uniq := h}⟩,
+ λ ⟨h⟩, by exactI fintype.card_unique⟩
+
 /-- A `fintype` with cardinality zero is equivalent to `empty`. -/
 def card_eq_zero_equiv_equiv_empty : card α = 0 ≃ (α ≃ empty) :=
 (equiv.of_iff card_eq_zero_iff).trans (equiv.equiv_empty_equiv α).symm

src/linear_algebra/matrix/determinant.lean

@@ -86,21 +86,16 @@ end
 @[simp] lemma det_one : det (1 : matrix n n R) = 1 :=
 by rw [← diagonal_one]; simp [-diagonal_one]
 
+@[simp]
+lemma det_is_empty [is_empty n] {A : matrix n n R} : det A = 1 :=
+by simp [det_apply]
+
 lemma det_eq_one_of_card_eq_zero {A : matrix n n R} (h : fintype.card n = 0) : det A = 1 :=
 begin
-  have perm_eq : (univ : finset (perm n)) = {1} :=
-  univ_eq_singleton_of_card_one (1 : perm n) (by simp [card_univ, fintype.card_perm, h]),
-  simp [det_apply, card_eq_zero.mp h, perm_eq],
+  haveI : is_empty n := fintype.card_eq_zero_iff.mp h,
+  exact det_is_empty,
 end
 
-/-- Specialize `det_eq_one_of_card_eq_zero` to `fin 0`.
-
-This is especially useful in combination with the `det_succ_` lemmas,
-for computing the determinant of a matrix given in the `![...]` notation.
--/
-@[simp] lemma det_fin_zero {A : matrix (fin 0) (fin 0) R}: det A = 1 :=
-det_eq_one_of_card_eq_zero (fintype.card_fin _)
-
 /-- If `n` has only one element, the determinant of an `n` by `n` matrix is just that element.
 Although `unique` implies `decidable_eq` and `fintype`, the instances might
 not be syntactically equal. Thus, we need to fill in the args explicitly. -/
@@ -112,11 +107,8 @@ by simp [det_apply, univ_unique]
 lemma det_eq_elem_of_card_eq_one {A : matrix n n R} (h : fintype.card n = 1) (k : n) :
   det A = A k k :=
 begin
-  have h1 : (univ : finset (perm n)) = {1},
-  { apply univ_eq_singleton_of_card_one (1 : perm n),
-    simp [card_univ, fintype.card_perm, h] },
-  have h2 := univ_eq_singleton_of_card_one k h,
-  simp [det_apply, h1, h2],
+  casesI fintype.card_eq_one_iff_nonempty_unique.mp h,
+  convert det_unique A,
 end
 
 lemma det_mul_aux {M N : matrix n n R} {p : n → n} (H : ¬bijective p) :