Mathlib v3 is deprecated. Go to Mathlib v4

Def opposite.op_induction

Modification history

2021-10-12 08:59
src/data/opposite.lean
refactor(data/opposite): Remove the `op_induction` tactic (#9660) …
Deleted opposite.op_inductionView on Github →
2019-05-17 06:56
src/data/opposite.lean
chore(opposites): merge two definitions of `opposite` (#1036) …
Added opposite.op_inductionView on Github →