Def Sum.Lex.inrLatticeHom

Modification history

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