isSMulRegular_on_quot_iff_lsmul_comap_eq

English

IsSMulRegular on the quotient M/N by r is equivalent to comap equality: N.comap (lsmul R M r) = N.

Русский

IsSMulRegular на факторе M/N по r эквивалентно равенству comap: N.comap (lsmul R M r) = N.

LaTeX

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

Lean4

theorem isSMulRegular_on_quot_iff_lsmul_comap_eq : IsSMulRegular (M ⧸ N) r ↔ N.comap (LinearMap.lsmul R M r) = N :=
  Iff.trans (isSMulRegular_on_quot_iff_lsmul_comap_le N r) <| LE.le.ge_iff_eq' (fun _ => N.smul_mem r)

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