Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.sum_assoc_apply_in1

Modification history

2022-01-08 07:22

src/data/equiv/basic.lean

feat(data/sum/order): Linear and disjoint sums of orders (#11157) …

Deleted equiv.sum_assoc_apply_in1 View on Github →

2017-12-17 02:45

data/equiv.lean

feat(data/ordinal): ordinal collapse, ordinals ordering,

Added equiv.sum_assoc_apply_in1 View on Github →