Theorem Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson

Modification history

2023-05-18 05:52
Mathlib/RingTheory/JacobsonIdeal.lean
feat port RingTheory.JacobsonIdeal (#4061)
Added Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobsonView on Github →