mathlib3
9bf23b0a - feat(order/initial_seg): Initial/principal segment from empty type (#15375)

Commit

3 years ago

feat(order/initial_seg): Initial/principal segment from empty type (#15375)

Author

vihdzp

vihdzp

Parents

Loading