Skip to content

chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas#5969

Merged
kim-em merged 3 commits intomasterfrom
upstream_insertIdx
Nov 6, 2024
Merged

chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas#5969
kim-em merged 3 commits intomasterfrom
upstream_insertIdx

Commits

Commits on Nov 6, 2024