map_jacobson_of_ker_le — Mathlib

English

If ker f ≤ jacobson R, then Submodule.map f(jacobson R) = jacobson R₂.

Русский

Если ker f ≤ jacobson R, тогда образ jacobson R равен jacobson R₂.

LaTeX

$$$\\ker f \\le \\operatorname{jacobson}(R) \\Rightarrow \\operatorname{Submodule.map}_{f}(\\operatorname{jacobson}(R)) = \\operatorname{jacobson}(R_2).$$$

Lean4

theorem map_jacobson_of_ker_le (le : RingHom.ker f ≤ jacobson R) :
    Submodule.map f.toSemilinearMap (jacobson R) = jacobson R₂ :=
  Module.map_jacobson_of_ker_le f.surjective le

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