[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ Matrix.det ↑A * Matrix.det ↑A⁻¹ = 1
[PROOFSTEP]
rw [← det_mul, A.mul_inv, det_one]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ Matrix.det ↑A⁻¹ * Matrix.det ↑A = 1
[PROOFSTEP]
rw [← det_mul, A.inv_mul, det_one]
[GOAL]
n : Type u
R : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrderedCommRing R
inst✝ : Fact (Even (Fintype.card n))
g : { x // x ∈ GLPos n R }
⊢ -↑g ∈ GLPos n R
[PROOFSTEP]
rw [mem_glpos, GeneralLinearGroup.det_apply_val, Units.val_neg, det_neg,
  (Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]
[GOAL]
n : Type u
R : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrderedCommRing R
inst✝ : Fact (Even (Fintype.card n))
g : { x // x ∈ GLPos n R }
⊢ 0 < det ↑↑g
[PROOFSTEP]
exact g.prop
[GOAL]
R : Type ?u.1604470
inst✝ : Field R
a b : R
hab : a ^ 2 + b ^ 2 ≠ 0
⊢ det (↑of ![![a, -b], ![b, a]]) ≠ 0
[PROOFSTEP]
simpa [det_fin_two, sq] using hab
