Mathlib v3 is deprecated. Go to Mathlib v4

Theorem opposite.op_inj_iff

Modification history

2022-06-27 16:25

src/data/opposite.lean

feat(*): Upgrade to lean 3.44.1c (#14984) …

Modified opposite.op_inj_iff View on Github →

2019-11-12 03:02

src/data/opposite.lean

chore(*): use `iff.rfl` instead of `iff.refl _` (#1675)

Modified opposite.op_inj_iff View on Github →

2019-06-29 13:28

src/data/opposite.lean

refactor(category_theory/category): reorder arguments of `End.has_mul` (#1128) …

Added opposite.op_inj_iff View on Github →