English
For f: M → M linear over R and A a commutative ring with an R-algebra structure, det(f.baseChange A) = algebraMap_R_A (det f).
Русский
Для отображения f: M → M над R и кольца A с структурой R-алгебры, det(f.baseChange A) = algebraMap_R_A (det f).
LaTeX
$$$\operatorname{det}(f.baseChange A) = \operatorname{algebraMap} R A (\operatorname{det} f).$$$
Lean4
theorem det_baseChange {R M} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {A}
[CommRing A] [Algebra R A] (f : M →ₗ[R] M) : LinearMap.det (f.baseChange A) = algebraMap R A (LinearMap.det f) :=
by
nontriviality A
have := (algebraMap R A).domain_nontrivial
rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]
simp
