Mathlib v3 is deprecated. Go to Mathlib v4

Theorem relator.bi_total_eq

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.bi_total_eq View on Github →