Revision #1178 → #1723 · back to history
addedExponent of one is the base02fbae2bab20
modifiedSubstitution property of equalitybb08b6259748
| Field | From #1178 | To #1723 |
|---|
| mathlib.module | — | Init.Prelude |
modifiedTransitivity of inequalities268d8501ed10
| Field | From #1178 | To #1723 |
|---|
| mathlib.module | — | Mathlib.Order.Defs.PartialOrder |
| note | lt_trans (and le_trans, aliased in Mathlib.Order.Basic) give transitivity of strict and non-strict inequalities. | lt_trans (and le_trans) give transitivity of strict and non-strict inequalities. |
modifiedReversing an inequation68160e914003
| Field | From #1178 | To #1723 |
|---|
| mathlib.module | — | Init.Core |