Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-12-17 02:45
b19c222c
View on Github →
feat(data/ordinal): ordinal collapse, ordinals ordering,
Estimated changes
Modified
algebra/group_power.lean
Modified
data/cardinal.lean
added
theorem
cardinal.embedding.sum_congr_apply_inl
added
theorem
cardinal.embedding.sum_congr_apply_inr
added
def
cardinal.mk
Modified
data/equiv.lean
added
def
equiv.empty_prod
added
def
equiv.empty_sum
added
theorem
equiv.prod_congr_apply
added
def
equiv.prod_empty
deleted
def
equiv.prod_empty_left
deleted
def
equiv.prod_empty_right
added
def
equiv.prod_unit
deleted
def
equiv.prod_unit_left
deleted
def
equiv.prod_unit_right
added
theorem
equiv.sum_assoc_apply_in1
added
theorem
equiv.sum_assoc_apply_in2
added
theorem
equiv.sum_assoc_apply_in3
added
theorem
equiv.sum_congr_apply_inl
added
theorem
equiv.sum_congr_apply_inr
added
def
equiv.sum_empty
deleted
def
equiv.sum_empty_left
deleted
def
equiv.sum_empty_right
added
def
equiv.unit_prod
Modified
data/ordinal.lean
added
def
cardinal.ord
added
theorem
cardinal.ord_eq
added
theorem
cardinal.ord_eq_min
added
theorem
cardinal.ord_le
added
theorem
cardinal.ord_le_ord
added
def
initial_seg.le_add
added
theorem
initial_seg.le_add_apply
added
def
order_embedding.collapse
added
theorem
order_embedding.collapse_F.lt
added
theorem
order_embedding.collapse_F.not_lt
added
def
order_embedding.collapse_F
added
theorem
order_embedding.collapse_apply
added
def
order_embedding.of_monotone
deleted
theorem
order_embedding.of_monotone
added
theorem
order_embedding.of_monotone_coe
added
def
order_embedding.preimage
added
theorem
ordinal.add_le_add_iff_left
added
theorem
ordinal.add_le_add_left
added
theorem
ordinal.add_succ
added
theorem
ordinal.card_add
added
theorem
ordinal.card_le_card
added
theorem
ordinal.card_one
added
theorem
ordinal.card_zero
added
theorem
ordinal.le_add_left
added
theorem
ordinal.le_add_right
added
theorem
ordinal.le_min
added
theorem
ordinal.le_total
added
def
ordinal.min
added
theorem
ordinal.min_eq
added
theorem
ordinal.min_le
added
def
ordinal.succ
added
theorem
ordinal.type_le_of_order_embedding
added
theorem
ordinal.zero_le
deleted
def
prod.lex.is_well_order
deleted
def
sum.lex.is_well_order
added
theorem
well_founded.has_min
added
def
well_founded.min
added
theorem
well_founded.min_mem
added
theorem
well_founded.not_lt_min
Modified
data/set/basic.lean
modified
theorem
set.mem_range
added
theorem
set.mem_range_self
Modified
logic/basic.lean
added
def
empty.elim
deleted
theorem
empty.elim
Modified
order/complete_lattice.lean
Modified
tactic/alias.lean
Modified
tactic/interactive.lean