Commit 2023-11-16 14:12 48237d43

View on Github →

style: cleanup some autoImplicits (#8288) In some cases adding the arguments manually results in a more obvious argument order anyway

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/MinimalAxioms.lean

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

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

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

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/NeZero.lean

Modified Mathlib/Algebra/Invertible/Defs.lean

modified theorem invOf_mul_eq_iff_eq_mul_left

modified theorem mul_invOf_eq_iff_eq_mul_right

modified theorem mul_left_eq_iff_eq_invOf_mul

modified theorem mul_left_inj_of_invertible

modified theorem mul_right_eq_iff_eq_mul_invOf

modified theorem mul_right_inj_of_invertible

Modified Mathlib/Algebra/Invertible/GroupWithZero.lean

Modified Mathlib/Algebra/Opposites.lean