English
In a setting with a block decomposition of a matrix and an auxiliary matrix auxMat, the norm of a product can be computed by tracking block-triangular forms and corner blocks; this yields determinant identities decomposing the full determinant into simpler pieces.
Русский
При разложении матрицы на блоки и введении дополнительной матрицы auxMat норму произведения можно посчитать через треугольность по блокам и угловые блоки; это даёт тождества относительно детерминантов, разлагающих полный детерминант на простые части.
LaTeX
$$$ $$$
Lean4
/-- The norm of an element `s` of an `R`-algebra is the determinant of `(*) s`. -/
@[stacks 0BIF "Norm"]
noncomputable def norm : S →* R :=
LinearMap.det.comp (lmul R S).toRingHom.toMonoidHom
