Commit 2023-10-30 21:42 57cf5ffa

View on Github →

chore: refactor to List.get (#8039)

Estimated changes

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Combinatorics/Composition.lean

modified def Composition.blocksFun

modified theorem Composition.blocks_pos'

modified theorem Composition.one_le_blocks'

added theorem List.get_splitWrtComposition'

added theorem List.get_splitWrtCompositionAux

deleted theorem List.nthLe_splitWrtComposition

deleted theorem List.nthLe_splitWrtCompositionAux