Commit 2024-04-05 17:00 eb959642

View on Github →

chore: Homogenise instances for MulOpposite/AddOpposite (#11485) by declaring them all in where style with implicit type assumptions and inst prefix Here to reduce the diff from #11203

Estimated changes

modified theorem AddOpposite.op_div
modified theorem AddOpposite.op_eq_one_iff
modified theorem AddOpposite.op_inv
modified theorem AddOpposite.op_mul
modified theorem AddOpposite.op_one
modified theorem AddOpposite.unop_div
modified theorem AddOpposite.unop_eq_one_iff
modified theorem AddOpposite.unop_inv
modified theorem AddOpposite.unop_mul
modified theorem AddOpposite.unop_one
modified theorem MulOpposite.op_add
modified theorem MulOpposite.op_eq_one_iff
modified theorem MulOpposite.op_inv
modified theorem MulOpposite.op_mul
modified theorem MulOpposite.op_neg
modified theorem MulOpposite.op_one
modified theorem MulOpposite.op_smul
modified theorem MulOpposite.op_sub
modified theorem MulOpposite.op_zero
modified theorem MulOpposite.unop_add
modified theorem MulOpposite.unop_inv
modified theorem MulOpposite.unop_mul
modified theorem MulOpposite.unop_neg
modified theorem MulOpposite.unop_one
modified theorem MulOpposite.unop_smul
modified theorem MulOpposite.unop_sub
modified theorem MulOpposite.unop_zero
modified def MulOpposite
modified structure PreOpposite