matrix — Mathlib

English

If k is IsSMulRegular in S, then the matrix space over S is IsSMulRegular with the same k; i.e., regularity is preserved when passing to matrices.

Русский

Если k является IsSMulRegular в S, то пространство матриц над S также IsSMulRegular для того же k; регулярность сохраняется при переходе к матрицам.

LaTeX

$$$ IsSMulRegular(S,k) \\Rightarrow IsSMulRegular( Matrix(m,n,S), k ) $$$

Lean4

theorem _root_.IsSMulRegular.matrix [SMul R S] {k : R} (hk : IsSMulRegular S k) : IsSMulRegular (Matrix m n S) k :=
  IsSMulRegular.pi fun _ => IsSMulRegular.pi fun _ => hk

Похожие утверждения