mem_of_isSMulRegular_quotient_of_smul_mem

English

If IsSMulRegular on the quotient M/N by r holds, then for every x in M with r · x ∈ N we have x ∈ N.

Русский

Если IsSMulRegular на фактор-модуле M/N по r выполняется, то для каждого x ∈ M с r · x ∈ N имеет место x ∈ N.

LaTeX

$$$IsSMulRegular(M/N)\, r \Rightarrow (\forall x \in M,\ r \cdot x \in N \Rightarrow x \in N)$$$

Lean4

theorem mem_of_isSMulRegular_quotient_of_smul_mem (h1 : IsSMulRegular (M ⧸ N) r) {x : M} (h2 : r • x ∈ N) : x ∈ N :=
  (isSMulRegular_quotient_iff_mem_of_smul_mem N r).mp h1 x h2

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