mathlib

4b00aa2d - refactor(ring_theory/jacobson): avoid shadowing hypothesis (#9736)

refactor(ring_theory/jacobson): avoid shadowing hypothesis (#9736) This PR postpones a `rw` in a proof, which was creating a shadowed hypothesis. At present, this shadowing was not a big deal, but in another branch it caused a hard-to-diagnose error. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>