Commit 2024-09-26 12:41 bcb7eb27

View on Github →

chore: remove List.ofFn lemmas moved to Batteries (#17159)

Estimated changes

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/OfFn.lean

deleted theorem List.getElem?_ofFn

deleted theorem List.getElem_ofFn

deleted theorem List.getElem_ofFn_go

deleted theorem List.get_ofFn_go

deleted theorem List.length_ofFn

deleted theorem List.length_ofFn_go

Modified lake-manifest.json