Commit 2024-06-18 17:35 6f05744d

View on Github →

feat: generalize Set.inv_mem_center (#13921) From #13034.

Estimated changes

Modified Mathlib/Algebra/Group/Center.lean

modified theorem Set.div_mem_center

modified theorem Set.inv_mem_center

modified theorem Set.inv_mem_center₀

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