Commit 2024-05-17 17:53 f933e98b

View on Github →

feat(Order/RelSeries): add snoc construction (#12915) Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ and an a such that aₙ -r→ a holds, there is a series of length n+1: a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a. These and some other lemmas in this PR are all extracted from Order/JordanHolder.lean

Estimated changes