Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-05 05:18 98dbe27a

View on Github →

feat(algebra/opposites): add some trivial @[simp] lemmas (#1508)

Estimated changes

added theorem opposite.op_add
added theorem opposite.op_inv
added theorem opposite.op_mul
added theorem opposite.op_neg
added theorem opposite.op_one
added theorem opposite.op_zero
added theorem opposite.unop_add
added theorem opposite.unop_inv
added theorem opposite.unop_mul
added theorem opposite.unop_neg
added theorem opposite.unop_one
added theorem opposite.unop_zero