Theorem MulOpposite.Commute.unop

Modification history

2023-12-04 10:29
Mathlib/Algebra/Group/Opposite.lean
fix(Tactic/ToAdditive): handle `AddCommute` and `AddSemiconjBy` correctly (#8757) …
Deleted MulOpposite.Commute.unopView on Github →
2022-12-12 02:05
Mathlib/Algebra/Group/Opposite.lean
feat: port algebra.group.opposite (#912) …
Added MulOpposite.Commute.unopView on Github →