Commit 2024-01-05 11:32 c8d50df1

View on Github →

chore: Move Commute results earlier (#9440) These lemmas aren't really proved any faster using units, and I will soon need them not to be proved using units. Part of #9411

Estimated changes

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

added theorem Commute.inv_left_iff

added theorem Commute.inv_mul_cancel_assoc

added theorem Commute.inv_right_iff

Modified Mathlib/Algebra/Group/Commute/Units.lean

deleted theorem Commute.inv_left

deleted theorem Commute.inv_left_iff

deleted theorem Commute.inv_mul_cancel_assoc

deleted theorem Commute.inv_right

deleted theorem Commute.inv_right_iff

deleted theorem inv_mul_cancel_comm

deleted theorem inv_mul_cancel_comm_assoc

Modified Mathlib/Algebra/Group/Defs.lean

added theorem inv_mul_cancel_comm

added theorem inv_mul_cancel_comm_assoc

added theorem zpow_coe_nat

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

deleted theorem SemiconjBy.inv_inv_symm

modified theorem SemiconjBy.inv_inv_symm_iff

added theorem SemiconjBy.inv_right_iff

added theorem SemiconjBy.inv_symm_left_iff

Modified Mathlib/Algebra/Group/Semiconj/Units.lean

deleted theorem SemiconjBy.inv_right

deleted theorem SemiconjBy.inv_right_iff

deleted theorem SemiconjBy.inv_symm_left

deleted theorem SemiconjBy.inv_symm_left_iff

Modified Mathlib/Algebra/GroupPower/Basic.lean

Modified Mathlib/Data/Int/Basic.lean

deleted theorem zpow_coe_nat