Theorem NonemptyInterval.toProd_injective

Modification history

2023-11-16 19:44

Mathlib/Order/Interval.lean

style: cleanup by putting `by` on the same line as `:=` (#8407)

Modified NonemptyInterval.toProd_injective View on Github →

2023-05-22 16:35

Mathlib/Order/Interval.lean

feat: port Order.Interval (#3360)

Added NonemptyInterval.toProd_injective View on Github →