isSMulRegular_of_ker_lsmul_eq_bot

English

If the kernel of the left action by r on M is {0}, then r is a regular scalar on M.

Русский

Если ядро левого действия на M равняется нулю, то r — регулярный скаляр на M.

LaTeX

$$$\ker(\operatorname{lsmul} R M r) = \{0\} \Rightarrow IsSMulRegular M r$$$

Lean4

theorem isSMulRegular_of_ker_lsmul_eq_bot (h : LinearMap.ker (LinearMap.lsmul R M r) = ⊥) : IsSMulRegular M r :=
  (isSMulRegular_iff_ker_lsmul_eq_bot M r).mpr h

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