Commit 2025-06-02 00:01 ac7d8cf0

View on Github →

chore: deprime induction in Computability and FieldTheory (#25198) As well as the one instance in Combinatorics and the one instance in Control.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Computability/DFA.lean

Modified Mathlib/Computability/Encoding.lean

modified theorem Computability.decode_encodePosNum

Modified Mathlib/Computability/EpsilonNFA.lean

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Computability/NFA.lean

Modified Mathlib/Computability/Partrec.lean

Modified Mathlib/Computability/PartrecCode.lean

Modified Mathlib/Computability/PostTuringMachine.lean

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Computability/TMConfig.lean

Modified Mathlib/Computability/TMToPartrec.lean

Modified Mathlib/Computability/Tape.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Control/LawfulFix.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

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

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

Modified Mathlib/FieldTheory/Separable.lean