Smooth matrix products #
Matrix multiplication preserves smoothness of families. This rule uses the usual finite-product norms, without choosing a matrix algebra norm, and supports smooth paths assembled from elementary matrices.
theorem
ContDiff.matrix_mul
{𝕜 : Type u_1}
{R : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing R]
[NormedAlgebra 𝕜 R]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
[Fintype m]
[Fintype n]
[Fintype p]
{k : WithTop ℕ∞}
{f : E → Matrix m n R}
{g : E → Matrix n p R}
(hf : ContDiff 𝕜 k f)
(hg : ContDiff 𝕜 k g)
:
The product of two smooth matrix families is smooth.