det_map — Mathlib

English

For a basis b and a linear equivalence f, and v: ι → M', the determinant of b.map f with respect to v equals the determinant of b with respect to f.symm applied to v.

Русский

Для базиса b и линейного отображения-дифференциала f, и вектора v:.det(b.map f по v) = det(b по (f.symm ∘ v))

LaTeX

$$ (b.map f).det v = b.det (f.symm ∘ v)$$

Lean4

@[simp]
theorem det_map (b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') : (b.map f).det v = b.det (f.symm ∘ v) := by
  rw [det_apply, toMatrix_map, det_apply]

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