Theorem Sum.Lex.inr_inf

Modification history

2023-11-08 20:09
Mathlib/Data/Sum/Lattice.lean
feat: Sum of lattices (#8181) …
Added Sum.Lex.inr_infView on Github →