English
For modules M that are free of finite rank and indexed maps f_i: ι → M →ₗ M, the determinant of the block-diagonal pi-map equals the product of the determinants: det(π) = ∏ det(f_i).
Русский
Для свободных конечно ранговых модулей M и отображений f_i: ι → M → M детерминант блока-подматрицы pi равен произведению детерминантов f_i.
LaTeX
$$$\det\left(\mathrm{pi}\; (f_i)\right) = \prod_i \det(f_i)$$$
Lean4
/-- On a `LinearEquiv`, the domain of `LinearMap.det` can be promoted to `Rˣ`. -/
protected def det : (M ≃ₗ[R] M) →* Rˣ :=
(Units.map (LinearMap.det : (M →ₗ[R] M) →* R)).comp
(LinearMap.GeneralLinearGroup.generalLinearEquiv R M).symm.toMonoidHom
