Commit 2025-07-31 17:11 ef7b38bb

View on Github →

chore: move and golf Subring.mem_closure_image_of (#27652)

Estimated changes

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

added theorem Subring.mem_closure_image_of

Modified Mathlib/RingTheory/Jacobson/Ring.lean

deleted theorem Polynomial.Subring.mem_closure_image_of