Mathlib v3 is deprecated. Go to Mathlib v4

Def sum3.in₁

Modification history

2022-05-05 05:36
src/data/sum/basic.lean
feat(data/sum/basic): Shortcuts for the ternary sum of types (#13678) …
Added sum3.in₁View on Github →