Commit 2022-11-24 21:48 ad9d93b1

View on Github →

feat: port Algebra.Opposites (#644) mathlib SHA: fd47bdf09e90f553519c712378e651975fe8c829

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Opposites.lean

added theorem AddOpposite.op_div

added theorem AddOpposite.op_eq_one_iff

added theorem AddOpposite.op_inv

added theorem AddOpposite.op_mul

added theorem AddOpposite.op_one

added theorem AddOpposite.unop_div

added theorem AddOpposite.unop_eq_one_iff

added theorem AddOpposite.unop_inv

added theorem AddOpposite.unop_mul

added theorem AddOpposite.unop_one

added def MulOpposite.op

added def MulOpposite.opEquiv

added theorem MulOpposite.op_add

added theorem MulOpposite.op_bijective

added theorem MulOpposite.op_comp_unop

added theorem MulOpposite.op_eq_one_iff

added theorem MulOpposite.op_eq_zero_iff

added theorem MulOpposite.op_inj

added theorem MulOpposite.op_injective

added theorem MulOpposite.op_inv

added theorem MulOpposite.op_mul

added theorem MulOpposite.op_ne_zero_iff

added theorem MulOpposite.op_neg

added theorem MulOpposite.op_one

added theorem MulOpposite.op_smul

added theorem MulOpposite.op_sub

added theorem MulOpposite.op_surjective

added theorem MulOpposite.op_unop

added theorem MulOpposite.op_zero

added def MulOpposite.unop

added theorem MulOpposite.unop_add

added theorem MulOpposite.unop_bijective

added theorem MulOpposite.unop_comp_op

added theorem MulOpposite.unop_eq_one_iff

added theorem MulOpposite.unop_eq_zero_iff

added theorem MulOpposite.unop_inj

added theorem MulOpposite.unop_injective

added theorem MulOpposite.unop_inv

added theorem MulOpposite.unop_mul

added theorem MulOpposite.unop_ne_zero_iff

added theorem MulOpposite.unop_neg

added theorem MulOpposite.unop_one

added theorem MulOpposite.unop_op

added theorem MulOpposite.unop_smul

added theorem MulOpposite.unop_sub

added theorem MulOpposite.unop_surjective

added theorem MulOpposite.unop_zero

added def MulOpposite

Modified Mathlib/Logic/Equiv/Defs.lean