mathlib

3402608c - Merge branch 'rel_embedding_empty' into initial_seg_golf