subsingleton_of_subsingleton — Mathlib

English

If the index type n is a singleton, then SL(n,R) is a singleton as well.

Русский

Если индексный тип является одиночным, то SL(n,R) тоже одиночный.

LaTeX

$$Subsingleton (SpecialLinearGroup n R)$$

Lean4

instance subsingleton_of_subsingleton [Subsingleton n] : Subsingleton (SpecialLinearGroup n R) :=
  by
  refine ⟨fun ⟨A, hA⟩ ⟨B, hB⟩ ↦ ?_⟩
  ext i j
  rcases isEmpty_or_nonempty n with hn | hn; · exfalso; exact IsEmpty.false i
  rw [det_eq_elem_of_subsingleton _ i] at hA hB
  simp only [Subsingleton.elim j i, hA, hB]

Похожие утверждения