Skip to content

feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone#41617

Open
joelriou wants to merge 1 commit into
leanprover-community:masterfrom
joelriou:fin-insertnth-monotone
Open

feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone#41617
joelriou wants to merge 1 commit into
leanprover-community:masterfrom
joelriou:fin-insertnth-monotone

feat(Order/Fin): conditions for `Fin.insertNth` to be monotone or str…

a39b5f0
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
label-and-report-new-contributor
succeeded Jul 11, 2026 in 4s