Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-03 20:19 3f5ec68c

View on Github →

fix(*): make three trans_applys rfl-lemmas

Estimated changes

Modified data/equiv/basic.lean

modified theorem equiv.trans_apply

Modified order/order_iso.lean

modified theorem order_embedding.trans_apply

Modified set_theory/ordinal.lean

modified theorem initial_seg.trans_apply