Commit 2026-10-06 12:30 eb681fbd

View on Github →

chore(FieldTheory/IntermediateField/Adjoin): fix recursors (#42856) Name the motive motive and name the minor premises according to their contents. Also make the motive implicit.

Estimated changes

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

modified theorem IntermediateField.induction_on_adjoin

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

modified theorem IntermediateField.adjoin_induction

modified theorem IntermediateField.induction_on_adjoin_fg

modified theorem IntermediateField.induction_on_adjoin_finset

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean