jacobson_quotient_of_le — Mathlib

English

For any submodule N ≤ jacobson R M, jacobson R (M ⧸ N) = map N.mkQ (jacobson R M).

Русский

Для любого подмодуля N ≤ jacobson(R,M) выполняется jacobson(R, M/N) = map N.mkQ (jacobson(R,M)).

LaTeX

$$le ⇒ jacobson R (M ⧸ N) = map N.mkQ (jacobson R M)$$

Lean4

theorem jacobson_quotient_of_le {N : Submodule R M} (le : N ≤ jacobson R M) :
    jacobson R (M ⧸ N) = map N.mkQ (jacobson R M) :=
  (map_jacobson_of_ker_le N.mkQ_surjective <| by rwa [ker_mkQ]).symm

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