Skip to content

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

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

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

Annotations

1 warning

Backport

succeeded Nov 6, 2024 in 4s