Commit 2022-11-24 02:16 52042446

View on Github →

chore: to_additive adds instances (#678)

Estimated changes

Modified Mathlib/Algebra/CovariantAndContravariant.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/OrderSynonym.lean

Modified Mathlib/Algebra/Order/Group.lean

Modified Mathlib/Algebra/Order/Monoid.lean

Modified Mathlib/Algebra/PEmptyInstances.lean

Modified Mathlib/Tactic/ToAdditive.lean

added def ToAdditive.copyInstanceAttribute

added def ToAdditive.copySimpAttribute

Modified test/toAdditive.lean

added theorem Test.one_fooClass

added theorem Test.zero_fooClass