Commit 2023-09-06 04:50 3d1bfa5b

View on Github →

chore: ensure Ring/Defs doesn't depend on Group/Basic (#6956) In the basic algebraic hierarchy, the Defs files should ideally only depend on earlier Defs files, importing as little theory as possible. This PR makes some rearrangements so Ring.Defs can depend on Group.Defs rather than requiring Group.Basic.

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

deleted theorem eq_inv_of_mul_eq_one_left

deleted theorem inv_eq_of_mul_eq_one_left

Modified Mathlib/Algebra/Group/Defs.lean

added theorem eq_inv_of_mul_eq_one_left

added theorem inv_eq_of_mul_eq_one_left

Modified Mathlib/Algebra/Group/WithOne/Basic.lean

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

deleted theorem eq_of_sub_eq_zero'

deleted theorem pow_succ''

Modified Mathlib/Algebra/Ring/Defs.lean

deleted theorem mul_add_eq_mul_add_iff_sub_mul_add_eq

deleted theorem sub_mul_add_eq_of_mul_add_eq_mul_add

Modified Mathlib/Algebra/Ring/MinimalAxioms.lean

Modified Mathlib/Data/Nat/Choose/Central.lean