Commit 2024-03-21 08:50 b505e8e9

View on Github →

chore: rename away from 'def' (#11548) This will become an error in 2024-03-16 nightly, possibly not permanently.

Estimated changes

deleted theorem Asymptotics.IsLittleO.def
added theorem Polynomial.Monic.def'
deleted theorem Polynomial.Monic.def
deleted theorem Polynomial.IsRoot.def
added theorem Polynomial.Splits.def'
deleted theorem Polynomial.Splits.def
modified theorem SModEq.sub_mem
modified theorem SModEq.zero
deleted theorem IntervalIntegrable.def
added theorem IsGenericPoint.def'
deleted theorem IsGenericPoint.def