Def Opposite.op

Modification history

2024-05-08 18:28

Mathlib/Data/Opposite.lean

refactor(Opposite): `Opposite.mk` -> `Opposite.op` (#12636) …

Deleted Opposite.op View on Github →

2023-04-18 01:37

Mathlib/Data/Opposite.lean

chore: made Opposite a structure (#3193) …

Modified Opposite.op View on Github →

2022-11-20 06:29

Mathlib/Data/Opposite.lean

port: Data.Opposite (#650) …

Added Opposite.op View on Github →