det_comp — Mathlib

English

The determinant of the composition f ∘ v equals det(f) times det(v): det_e(f ∘ v) = det f · det_e(v).

Русский

Детерминант композиции f ∘ v равен произведению det(f) на det(v): det_e(f ∘ v) = det(f) · det_e(v).

LaTeX

$$e.det (f ∘ v) = (LinearMap.det f) * e.det v$$

Lean4

@[simp]
theorem det_comp (e : Basis ι A M) (f : M →ₗ[A] M) (v : ι → M) : e.det (f ∘ v) = (LinearMap.det f) * e.det v := by
  rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul, e.toMatrix_eq_toMatrix_constr (f ∘ v),
    e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp, e.constr_comp]

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