isSMulRegular_of_isSMulRegular_on_submodule_on_quotient

English

If N is a submodule of M and r ∈ R is regular on N and on the quotient M/N, then r is regular on M.

Русский

Если N — подмодуль M и r ∈ R регулярен на N и на факторе M/N, то r регулярен и на M.

LaTeX

$$$IsSMulRegular(N,r) \Rightarrow (IsSMulRegular(M,N,r) \Rightarrow IsSMulRegular(M,r)).$$$

Lean4

theorem isSMulRegular_of_isSMulRegular_on_submodule_on_quotient (h1 : IsSMulRegular N r)
    (h2 : IsSMulRegular (M ⧸ N) r) : IsSMulRegular M r :=
  isSMulRegular_of_range_eq_ker N.injective_subtype (N.range_subtype.trans N.ker_mkQ.symm) h1 h2

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