Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-06 18:49 f18278de

View on Github →

chore(algebra/opposites): use injective.* constructors (#10200)

Estimated changes

modified theorem opposite.op_sub
modified theorem opposite.unop_sub