detAux_comp — Mathlib

English

For a fixed basis b of a finite free module M over a commutative ring A, the determinant is multiplicative with respect to composition: det_b(f ∘ g) = det_b(f) · det_b(g).

Русский

Для фиксированного базиса b конечного свободного A-модуля M выполняется равенство детерминанта при композиции линейных отображений: det_b(f ∘ g) = det_b(f) · det_b(g).

LaTeX

$$$\det_b(f \circ g) = \det_b(f) \cdot \det_b(g)$$$

Lean4

@[simp]
theorem detAux_comp (b : Trunc <| Basis ι A M) (f g : M →ₗ[A] M) :
    LinearMap.detAux b (f.comp g) = LinearMap.detAux b f * LinearMap.detAux b g :=
  (LinearMap.detAux b).map_mul f g

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