Commit 2022-12-20 05:33 70c8a66c

View on Github →

feat: make MulOpposite and AddOpposite structures (#1036) This refactor makes αᵐᵒᵖ and αᵃᵒᵖ into structures with one field, an idea more appropriate in Lean 4 than the Lean 3 approach of type synonyms.

Estimated changes

Modified Mathlib/Algebra/Group/Opposite.lean

Modified Mathlib/Algebra/Opposites.lean

modified theorem AddOpposite.unop_div

added structure AddOpposite

deleted def MulOpposite.op

modified theorem MulOpposite.op_inj

deleted def MulOpposite.unop

modified theorem MulOpposite.unop_op

added structure MulOpposite

deleted def MulOpposite

Modified Mathlib/Algebra/Ring/Opposite.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean