instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL

English

For Γ ⊆ SL(n,R), (Γ.map mapGL) hasDetOne.

Русский

Для Γ ⊆ SL(n,R) тождественное отображение детерминанта на отображение mapGL сохраняет детерминант равным единице.

LaTeX

$$$\forall {\Gamma} \; (\Gamma \subset SL(n,R)) \Rightarrow (Γ.map mapGL).HasDetOne$$$

Lean4

instance {S : Type*} [CommRing S] [Algebra S R] (Γ : Subgroup (SL n S)) : HasDetOne (Γ.map <| mapGL R) where
  det_eq {g} hg := by rcases hg with ⟨g, hg, rfl⟩; simp

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