Commit 2026-07-22 17:55 0c60917e
View on Github →fix(GroupTheory/Coprod): fix recursor argument name (#41930)
Fix the argument names of Monoid.Coprod.induction_on' and Monoid.Coprod.induction_on. Name the motive motive and name the minor premises according to their contents.