Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 20:48 b560d401

View on Github →

feat(data/sum/basic): sum.lift_rel is a subrelation of sum.lex (#15358) Also trivial spacing fix.

Estimated changes

modified theorem sum.lex.mono_right