mathlib3
b560d401 - feat(data/sum/basic): `sum.lift_rel` is a subrelation of `sum.lex` (#15358)

Commit
3 years ago
feat(data/sum/basic): `sum.lift_rel` is a subrelation of `sum.lex` (#15358) Also trivial spacing fix.
Author
Parents
Loading