Mathlib v3 is deprecated. Go to Mathlib v4

Theorem relator.left_unique.flip

Modification history

2021-09-15 13:22

src/logic/relator.lean

refactor(logic/relator): turn *_unique and *_total into defs, not classes (#9135) …

Added relator.left_unique.flip View on Github →