Commit 2024-05-06 07:35 594e3733

View on Github →

chore: migrate from List.removeNth to List.eraseIdx (#12660)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.removeNth_eq_nthTail

Modified Mathlib/Data/List/InsertNth.lean

added theorem List.eraseIdx_insertNth

added theorem List.insertNth_eraseIdx_of_ge

added theorem List.insertNth_eraseIdx_of_le

deleted theorem List.insertNth_removeNth_of_ge

deleted theorem List.insertNth_removeNth_of_le

deleted theorem List.removeNth_insertNth

Modified Mathlib/Data/Vector.lean

added def Vector.eraseIdx

deleted def Vector.removeNth

Modified Mathlib/Data/Vector/Basic.lean

added theorem Vector.eraseIdx_insertNth'

added theorem Vector.eraseIdx_insertNth

added theorem Vector.eraseIdx_val

deleted theorem Vector.removeNth_insertNth'

deleted theorem Vector.removeNth_insertNth

deleted theorem Vector.removeNth_val

Modified Mathlib/Init/Data/List/Lemmas.lean

Modified Mathlib/Logic/Function/Basic.lean

deleted theorem Function.id_def

Modified Mathlib/Testing/SlimCheck/Sampleable.lean

Modified Mathlib/Topology/List.lean

added theorem List.continuous_eraseIdx

deleted theorem List.continuous_removeNth

added theorem List.tendsto_eraseIdx

deleted theorem List.tendsto_removeNth

added theorem Vector.continuousAt_eraseIdx

deleted theorem Vector.continuousAt_removeNth

added theorem Vector.continuous_eraseIdx

deleted theorem Vector.continuous_removeNth

Modified lake-manifest.json