Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-04 09:05 0b7b912a

View on Github →

feat(set_theory/ordinal_notation): correctness of ordinal power

Estimated changes

Modified algebra/order.lean

modified theorem le_or_lt

Modified data/pnat.lean

added theorem nat.succ_pnat_coe

added theorem pnat.add_coe

added theorem pnat.eq

added theorem pnat.mk_coe

added theorem pnat.mul_coe

added theorem pnat.nat_coe_coe

deleted theorem pnat.nat_coe_val

modified theorem pnat.ne_zero

added theorem pnat.one_coe

added theorem pnat.pos

added def pnat.pow

deleted theorem pnat.to_pnat'_val

Modified logic/basic.lean

added theorem coe_coe

Modified set_theory/ordinal.lean

added theorem ordinal.add_le_add_iff_right

added theorem ordinal.add_lt_omega_power

added theorem ordinal.add_right_cancel

added theorem ordinal.add_sub_add_cancel

added theorem ordinal.dvd_add

added theorem ordinal.dvd_add_iff

added theorem ordinal.dvd_antisymm

added theorem ordinal.dvd_mul_of_dvd

added theorem ordinal.dvd_trans

added theorem ordinal.is_limit_iff_omega_dvd

added theorem ordinal.is_normal.limit_le

added theorem ordinal.le_of_dvd

added theorem ordinal.lt_limit

deleted theorem ordinal.mul_assoc

added theorem ordinal.mul_is_limit_left

added theorem ordinal.mul_lt_omega_power

added theorem ordinal.mul_omega_dvd

deleted theorem ordinal.mul_omega_power

deleted theorem ordinal.mul_one

added theorem ordinal.mul_sub

added theorem ordinal.nat_cast_succ

deleted theorem ordinal.one_mul

added theorem ordinal.power_dvd_power

added theorem ordinal.power_dvd_power_iff

added theorem ordinal.power_lt_omega

added theorem ordinal.power_omega

added theorem ordinal.sub_eq_of_add_eq

added theorem ordinal.sub_is_limit

added theorem ordinal.sub_sub

deleted theorem ordinal.succ_nat_cast

modified theorem ordinal.zero_dvd

Modified set_theory/ordinal_notation.lean

added def nonote.below

added def nonote.mk

added def nonote.oadd

added def nonote.power

added def nonote.rec_on

modified theorem nonote.repr_add

modified theorem nonote.repr_mul

added theorem nonote.repr_power

added theorem nonote.repr_sub

added theorem onote.NF.below_of_lt'

modified theorem onote.NF.below_of_lt

modified theorem onote.NF.fst

modified theorem onote.NF.oadd

added theorem onote.NF.of_dvd_omega

added theorem onote.NF.of_dvd_omega_power

modified theorem onote.NF.snd'

modified theorem onote.NF.snd

deleted theorem onote.NF.zero

added theorem onote.NF.zero_of_zero

modified def onote.NF

modified theorem onote.NF_below.fst

modified theorem onote.NF_below.lt

modified theorem onote.NF_below.oadd

modified theorem onote.NF_below.repr_lt

modified theorem onote.NF_below.snd

modified theorem onote.NF_below_iff_top_below

deleted theorem onote.NF_of_nat

added theorem onote.NF_repr_split'

added theorem onote.NF_repr_split

deleted theorem onote.add_NF

modified theorem onote.cmp_compares

modified theorem onote.le_def

modified theorem onote.lt_def

deleted theorem onote.mul_NF

added def onote.mul_nat

added theorem onote.mul_nat_eq_mul

added theorem onote.mul_zero

added theorem onote.oadd_add

modified theorem onote.oadd_lt_oadd_3

added theorem onote.oadd_mul

modified theorem onote.oadd_pos

added def onote.omega

modified theorem onote.omega_le_oadd

modified def onote.power_aux

added def onote.repr'

modified theorem onote.repr_add

modified theorem onote.repr_inj

modified theorem onote.repr_mul

added theorem onote.repr_power

added theorem onote.repr_power_aux₁

added theorem onote.repr_power_aux₂

added theorem onote.repr_scale

added theorem onote.repr_sub

modified def onote.scale

added theorem onote.scale_eq_mul

added theorem onote.scale_power_aux

modified def onote.split'

modified def onote.split

added theorem onote.split_add_lt

added theorem onote.split_dvd

added theorem onote.split_eq_scale_split'

added theorem onote.sub_NF_below

added def onote.to_string

added def onote.to_string_aux1

added theorem onote.zero_add

added theorem onote.zero_mul