Commit 2025-08-14 03:55 2b92f148

View on Github →

chore(Logic/Relation): induction case names (#28055) Name the motive motive and name the minor premises according to their case.

Estimated changes

Modified Mathlib/Logic/Relation.lean

modified theorem Relation.ReflTransGen.head_induction_on

modified theorem Relation.ReflTransGen.trans_induction_on

modified theorem Relation.TransGen.head_induction_on

modified theorem Relation.TransGen.trans_induction_on