Commit 2022-12-20 13:42 44741920

View on Github →

feat: port GroupTheory.GroupAction.Opposite (#1001) mathlib SHA : fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/Opposite.lean

added theorem MulOpposite.op_smul_eq_op_smul_op

added theorem MulOpposite.smul_eq_mul_unop

added theorem MulOpposite.unop_smul_eq_unop_smul_unop

added theorem op_smul_eq_mul