mathlib3
feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex`
#15368
Open
Overview
Commits
21
Changes
View On GitHub
Commits
  • move
    vihdzp committed 3 years ago
  • Update initial_seg.lean
    vihdzp committed 3 years ago
  • Update rel_iso.lean
    vihdzp committed 3 years ago
  • Update rel_iso.lean
    vihdzp committed 3 years ago
  • Merge branch 'principal_seg_move' into inl_initial_seg
    vihdzp committed 3 years ago
  • Merge branch 'rel_embedding_inl' into inl_initial_seg
    vihdzp committed 3 years ago
  • start
    vihdzp committed 3 years ago
  • Update initial_seg.lean
    vihdzp committed 3 years ago
  • Update initial_seg.lean
    vihdzp committed 3 years ago
  • Update arithmetic.lean
    vihdzp committed 3 years ago
  • Update initial_seg.lean
    vihdzp committed 3 years ago
  • Merge branch 'master' into inl_initial_seg
    vihdzp committed 3 years ago
  • Merge branch 'master' into inl_initial_seg
    vihdzp committed 3 years ago
  • fix
    vihdzp committed 3 years ago
  • revert stuff
    vihdzp committed 3 years ago
  • Merge branch 'master' into inl_initial_seg
    vihdzp committed 3 years ago
  • fix
    vihdzp committed 3 years ago
  • Merge branch 'master' into inl_initial_seg
    vihdzp committed 3 years ago
  • golf
    vihdzp committed 3 years ago
  • Update initial_seg.lean
    vihdzp committed 3 years ago
  • Merge branch 'master' into inl_initial_seg
    vihdzp committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading