English
Let b be a basis of M and b' a basis of M'. For a linear map f: M → M', the determinant of f with respect to bases b and b' equals det(f) times det(b' relative to b).
Русский
Пусть b — базис пространства M, b' — базис пространства M'. Для линейного отображения f: M → M' детерминант с отношением базисов b, b' равен det(f) умножить на det(b' относительно b).
LaTeX
$$b'.det (f ∘ b) = LinearMap.det f * b'.det b$$
Lean4
@[simp]
theorem det_comp_basis [Module A M'] (b : Basis ι A M) (b' : Basis ι A M') (f : M →ₗ[A] M') :
b'.det (f ∘ b) = LinearMap.det (f ∘ₗ (b'.equiv b (Equiv.refl ι) : M' →ₗ[A] M)) :=
by
rw [det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]
congr 1; ext i j
rw [toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]
