Commit 2025-09-24 03:26 a88dcfe0

View on Github →

chore: remove some 'nonrec' (#19907) nonrec is nearly always obfuscatory: it tells the reader "this apparent recursive call is not actually, but I'm going to leave you to guess what it is instead", when we could just disambiguate and tell the reader. However I'm not sure I have the patience to go through the remaining 600 uses. (A few are genuinely useful, but I guess less than 10%.)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean

added def ModuleCat.Derivation

Modified Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

added theorem PresheafOfModules.Derivation'.d_app

Modified Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

added def SimpContFract.of

Modified Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

added theorem ContFract.convs_eq_convs'

Modified Mathlib/Algebra/DualNumber.lean

added theorem DualNumber.algHom_ext

Modified Mathlib/Algebra/Quaternion.lean

added def Quaternion.im

added theorem Quaternion.im_add

added theorem Quaternion.im_neg

added theorem Quaternion.im_smul

added theorem Quaternion.im_sub

added theorem Quaternion.mul_star_eq_coe

added theorem Quaternion.re_add_im

added theorem Quaternion.self_add_star'

added theorem Quaternion.self_add_star

added theorem Quaternion.star_add_self'

added theorem Quaternion.star_add_self

added theorem Quaternion.star_eq_two_re_sub

added theorem Quaternion.star_mul_eq_coe

added theorem Quaternion.sub_im_self

added theorem Quaternion.sub_re_self