Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-12-18 08:38
f6bbca71
View on Github →
feat(data/ordinal): universe lifts, alephs
Estimated changes
Modified
algebra/big_operators.lean
added
theorem
finset.card_sigma
Modified
algebra/group_power.lean
added
theorem
nat.smul_eq_mul
Modified
algebra/module.lean
Modified
data/cardinal.lean
added
theorem
cardinal.add_one_le_succ
added
theorem
cardinal.fintype_card
added
theorem
cardinal.le_mk_iff_exists_set
added
def
cardinal.lift
added
theorem
cardinal.lift_add
added
theorem
cardinal.lift_id
added
theorem
cardinal.lift_inj
added
theorem
cardinal.lift_le
added
theorem
cardinal.lift_lift
added
theorem
cardinal.lift_lt
added
theorem
cardinal.lift_min
added
theorem
cardinal.lift_mk
added
theorem
cardinal.lift_mk_eq
added
theorem
cardinal.lift_mk_fin
added
theorem
cardinal.lift_mk_le
added
theorem
cardinal.lift_mul
added
theorem
cardinal.lift_nat_cast
added
theorem
cardinal.lift_one
added
theorem
cardinal.lift_power
added
theorem
cardinal.lift_umax
added
theorem
cardinal.lift_zero
added
theorem
cardinal.lt_succ_self
added
theorem
cardinal.mk_def
added
theorem
cardinal.mk_fin
added
theorem
cardinal.nat_cast_inj
added
theorem
cardinal.nat_cast_le
added
theorem
cardinal.nat_cast_lt
added
theorem
cardinal.nat_lt_ω
added
theorem
cardinal.nat_succ
added
def
cardinal.succ
added
theorem
cardinal.succ_le
modified
def
cardinal.ω
Modified
data/finset.lean
modified
theorem
finset.bind_mono
added
theorem
finset.card_image_of_inj_on
added
theorem
finset.card_image_of_injective
added
theorem
finset.card_product
Modified
data/fintype.lean
added
theorem
finset.eq_univ_iff_forall
modified
theorem
finset.mem_univ
modified
theorem
finset.mem_univ_val
added
theorem
fintype.card_bool
added
theorem
fintype.card_congr
added
theorem
fintype.card_empty
added
theorem
fintype.card_eq
added
theorem
fintype.card_fin
added
theorem
fintype.card_prod
added
theorem
fintype.card_sigma
added
theorem
fintype.card_sum
added
theorem
fintype.card_ulift
added
theorem
fintype.card_unit
modified
def
fintype.of_equiv
added
theorem
fintype.of_equiv_card
added
theorem
fintype.univ_bool
added
theorem
fintype.univ_empty
added
theorem
fintype.univ_unit
Modified
data/list/basic.lean
added
theorem
list.length_pmap
added
theorem
list.nth_le_index_of
Modified
data/multiset.lean
added
theorem
multiset.card_bind
added
theorem
multiset.card_join
added
theorem
multiset.card_map
added
theorem
multiset.card_pmap
added
theorem
multiset.card_product
added
theorem
multiset.card_sigma
Modified
data/ordinal.lean
added
theorem
cardinal.aleph_idx.init
added
def
cardinal.aleph_idx.initial_seg
added
theorem
cardinal.aleph_idx.initial_seg_coe
added
def
cardinal.aleph_idx.order_iso
added
theorem
cardinal.aleph_idx.order_iso_coe
added
def
cardinal.aleph_idx
added
theorem
cardinal.aleph_idx_le
added
theorem
cardinal.aleph_idx_lt
added
theorem
cardinal.card_ord
added
theorem
cardinal.lt_ord
added
def
cardinal.ord.order_embedding
added
theorem
cardinal.ord.order_embedding_coe
modified
theorem
cardinal.ord_eq_min
modified
theorem
cardinal.ord_le
modified
theorem
cardinal.ord_le_ord
added
theorem
cardinal.ord_le_type
added
theorem
cardinal.ord_lt_ord
added
theorem
cardinal.ord_zero
added
def
order.cof
deleted
theorem
order_iso.of_surjective_apply
added
theorem
order_iso.of_surjective_coe
added
theorem
order_iso.prod_lex_congr
added
theorem
order_iso.sum_lex_congr
added
def
ordinal.aleph'.order_iso
added
theorem
ordinal.aleph'.order_iso_coe
added
def
ordinal.aleph'
added
theorem
ordinal.aleph'_aleph_idx
added
theorem
ordinal.aleph'_le
added
theorem
ordinal.aleph'_lt
added
def
ordinal.aleph
added
theorem
ordinal.aleph_idx_aleph'
added
theorem
ordinal.card_nat
added
theorem
ordinal.card_type
added
def
ordinal.lift.initial_seg
added
theorem
ordinal.lift.initial_seg_coe
added
def
ordinal.lift.principal_seg
added
theorem
ordinal.lift.principal_seg_coe
added
theorem
ordinal.lift.principal_seg_top'
added
theorem
ordinal.lift.principal_seg_top
added
def
ordinal.lift
added
theorem
ordinal.lift_add
added
theorem
ordinal.lift_down
added
theorem
ordinal.lift_id
added
theorem
ordinal.lift_inj
added
theorem
ordinal.lift_le
added
theorem
ordinal.lift_lift
added
theorem
ordinal.lift_lt
added
theorem
ordinal.lift_min
added
theorem
ordinal.lift_mul
added
theorem
ordinal.lift_one
added
theorem
ordinal.lift_type_eq
added
theorem
ordinal.lift_type_le
added
theorem
ordinal.lift_type_lt
added
theorem
ordinal.lift_umax
added
theorem
ordinal.lift_zero
added
theorem
ordinal.lift_ω
added
theorem
ordinal.lt_succ_self
added
theorem
ordinal.ord_card_le
added
theorem
ordinal.type_le'
deleted
theorem
ordinal.type_le_of_order_embedding
added
def
ordinal.typein.principal_seg
added
theorem
ordinal.typein.principal_seg_coe
added
def
ordinal.ω