det_isUnitSMul — Mathlib

English

The determinant of a basis obtained by scaling each column by a unit is the product of these units.

Русский

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

LaTeX

$$e.det (e.unitsSMul w) = ∏ i, (w i : R)$$

Lean4

/-- The determinant of a basis constructed by `isUnitSMul` is the product of the given units. -/
@[simp]
theorem det_isUnitSMul {w : ι → R} (hw : ∀ i, IsUnit (w i)) : e.det (e.isUnitSMul hw) = ∏ i, w i :=
  e.det_unitsSMul_self _

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