Theorem Submodule.eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson

Modification history

2026-10-28 11:47
Mathlib/RingTheory/Nakayama.lean
chore(RingTheory/Jacobson): use `Ring.jacobson` throughout the library (#44788) …
Added Submodule.eq_of_map_mkQ_eq_map_mkQ_of_le_jacobsonView on Github →