Revision #3164 → #3659 · back to history
modifiedInteger division rounding modes (T/F-division)8ebd9b58733d
| Field | From #3164 | To #3659 |
|---|
| mathlib.module | Mathlib.Data.Int.Defs | Init.Data.Int.DivMod.Basic |
modifiedStructures allowing division by zero (zero ring, wheels)73e4ebbbeec9
| Field | From #3164 | To #3659 |
|---|
| mathlib.module | Mathlib.Algebra.Ring.Defs | Init.Core |
addedUniqueness in Euclidean division of naturals401be4c2ffa0
addedFractional part / mixed number6eb636df6d98
addedRational numbers as division extension of integers081f09cae1cd
addedLong division4d31d3be92bd
addedDivision algorithm referencec671681e32d7
addedDivision of rationals as multiplication by inverse37d82c39f093
addedPolynomial long division / synthetic division26d413fd4cfb
addedMoore–Penrose pseudoinverse4f491a88bf47
addedCancellative element98b04cf90577
addedIntegral domain18780ab8c040
addedZero ringf55756cb3f1b