mathlib3
feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex`
#15368

Open

feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex` #15368

vihdzp wants to merge 21 commits into master from inl_initial_seg

move

11451068

Update initial_seg.lean

b845ce4e

Update rel_iso.lean

77ce9129

Update rel_iso.lean

11e0ddd9

Merge branch 'principal_seg_move' into inl_initial_seg

f0906038

Merge branch 'rel_embedding_inl' into inl_initial_seg

f5f7d17b

start

e59170b1

Update initial_seg.lean

5ab6da87

Update initial_seg.lean

61a6fd0a

vihdzp added awaiting-review

vihdzp added blocked-by-other-PR

Update arithmetic.lean

80146393

Update initial_seg.lean

a879c9d4

Merge branch 'master' into inl_initial_seg

1744a74b

mathlib-dependent-issues-bot removed blocked-by-other-PR

Merge branch 'master' into inl_initial_seg

7369a986

fix

18e61568

revert stuff

cdf18f77

fpvandoorn added t-order

Merge branch 'master' into inl_initial_seg

af78c28b

vihdzp assigned

digama0 2 years ago

vihdzp added modifies-synchronized-file

fix

97056949

YaelDillies approved these changes on 2023-02-24

eric-wieser added merge-conflict

Merge branch 'master' into inl_initial_seg

084fa9b5

golf

993c33db

Update initial_seg.lean

ae6b8d4e

Merge branch 'master' into inl_initial_seg

ecc35f02

vihdzp removed merge-conflict

eric-wieser added not-too-late

Reviewers

YaelDillies

Assignees

digama0

Labels

awaiting-review t-order modifies-synchronized-file not-too-late

Milestone

No milestone

mathlib3 feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex` #15368 Open

feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex` #15368

mathlib3
feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex`
#15368

Open