Commit 2026-02-10 09:16 65590a2c

View on Github →

refactor(Data/List/Induction): improve definition of reverseRecOn (#33192) This PR improves the definition of List.reverseRecOn.

Estimated changes

Modified Mathlib/Data/List/Induction.lean

added def List.reverseRec

deleted def List.reverseRecOn

added theorem List.reverseRec_concat

added theorem List.reverseRec_nil