linearEquiv_det_conjAe — Mathlib

English

As a linear equivalence, conjAe has determinant -1 over the real numbers.

Русский

Как линейное эквивалентное отображение conjAe имеет детерминант -1 над R.

LaTeX

$$LinearEquiv.det conjAe.toLinearEquiv = -1.$$

Lean4

/-- The determinant of `conjAe`, as a linear equiv. -/
@[simp]
theorem linearEquiv_det_conjAe : LinearEquiv.det conjAe.toLinearEquiv = -1 := by
  rw [← Units.val_inj, LinearEquiv.coe_det, AlgEquiv.toLinearEquiv_toLinearMap, det_conjAe, Units.coe_neg_one]

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