Mathlib v3 is deprecated. Go to Mathlib v4

Def sum.swap

Modification history

2022-07-12 16:39
src/data/sum/basic.lean
chore(*): improve some definitional equalities (#15083) …
Modified sum.swapView on Github →
2018-01-11 23:22
data/sum.lean
doc(*): blurbs galore …
Modified sum.swapView on Github →
2017-12-13 04:31
data/sum.lean
feat(data/ordinal): well ordering theorem …
Added sum.swapView on Github →