Theorem RelSeries.toList_singleton

Modification history

2026-02-15 14:33
Mathlib/Order/RelSeries.lean
style: fix many leading by's in mathlib (#35343) …
Modified RelSeries.toList_singletonView on Github →
2025-05-19 08:29
Mathlib/Order/RelSeries.lean
chore(Order/RelSeries): induction principle for `RelSeries` (#22299) …
Added RelSeries.toList_singletonView on Github →