submodule — Mathlib

English

If N is a submodule of M and r is regular on M, then N inherits IsSmulRegular with the same r.

Русский

Если N — подподмодуль M и r регулярно действует на M, то N наследует IsSmulRegular с тем же r.

LaTeX

$$$\text{IsSmulRegular}(N,r) \Leftarrow \text{IsSmulRegular}(M,r)$ when N is a submodule.$$

Lean4

theorem submodule [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (r : R) (h : IsSMulRegular M r) :
    IsSMulRegular N r :=
  h.of_injective N.subtype N.injective_subtype

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