Commit 2025-03-29 00:17 9bda64ac

View on Github →

chore: review of induction branch names (#23358) Based on @eric-wieser's comment at https://github.com/leanprover-community/mathlib4/pull/23324#discussion_r2014688006. Induction principles to rename were found using the regex ^\s+\| @?[Hh]_. Most of this PR just removes h_ from the start of induction branch names that start with it, but MeasureTheory.SimpleFunc.induction and DirectSum.induction_(l)on receive more substantial changes, and the motive variables have been renamed to motive as per the naming conventions.

Estimated changes