isSMulRegular_on_quot_iff_lsmul_comap_le

English

IsSMulRegular on the quotient M/N by r is equivalent to the condition that N.comap (lsmul R M r) is contained in N.

Русский

Регулярность на факторе M/N по r эквивалентна условию, что N.comap(lsmul R M r) содержится в N.

LaTeX

$$$IsSMulRegular(M/N)\, r \iff N.{comap}(\operatorname{lsmul} R M r) \le N$$$

Lean4

theorem isSMulRegular_on_quot_iff_lsmul_comap_le : IsSMulRegular (M ⧸ N) r ↔ N.comap (LinearMap.lsmul R M r) ≤ N :=
  isSMulRegular_quotient_iff_mem_of_smul_mem N r

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