det_unitsSMul_self — Mathlib

English

The determinant of a mapped basis equals the determinant of the original basis composed with the inverse linear map.

Русский

Детерминант отображенного базиса равен детерминанту исходного базиса, композиционно с обратным линейным отображением.

LaTeX

$$ (b.map f).det = b.det.compLinearMap f.symm$$

Lean4

/-- The determinant of a basis constructed by `unitsSMul` is the product of the given units. -/
@[simp]
theorem det_unitsSMul_self (w : ι → Rˣ) : e.det (e.unitsSMul w) = ∏ i, (w i : R) := by simp [det_apply]

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