Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-03 21:23 5717986f

View on Github →

fix(*): update to lean also add mathlib nightly version to leanpkg.toml

Estimated changes

Modified algebra/archimedean.lean

Modified algebra/big_operators.lean

modified theorem finset.prod_const_one

added theorem finset.sum_const_zero

Modified algebra/group.lean

added def additive

added def multiplicative

Modified algebra/group_power.lean

added theorem add_gsmul

modified theorem add_monoid.add_smul

added theorem add_monoid.mul_smul'

added theorem add_monoid.mul_smul

modified theorem add_monoid.mul_smul_assoc

added theorem add_monoid.mul_smul_left

deleted theorem add_monoid.mul_smul_right

modified theorem add_monoid.neg_smul

modified theorem add_monoid.one_smul

added def add_monoid.smul

added theorem add_monoid.smul_add

modified theorem add_monoid.smul_eq_mul'

modified theorem add_monoid.smul_eq_mul

deleted theorem add_monoid.smul_mul

added theorem add_monoid.smul_neg_comm

modified theorem add_monoid.smul_nonneg

modified theorem add_monoid.smul_one

added theorem add_monoid.smul_sub

added theorem add_monoid.smul_zero

modified theorem add_monoid.zero_smul

added theorem bit0_gsmul

added theorem bit0_smul

added theorem bit1_gsmul

added theorem bit1_smul

modified def gpow

modified theorem gpow_add

modified theorem gpow_bit0

modified theorem gpow_bit1

modified theorem gpow_coe_nat

added theorem gpow_mul'

modified theorem gpow_mul

modified theorem gpow_mul_comm

modified theorem gpow_neg

modified theorem gpow_neg_one

added theorem gpow_neg_succ

added theorem gpow_of_nat

modified theorem gpow_one

modified theorem gpow_zero

added def gsmul

added theorem gsmul_add_comm

deleted theorem gsmul_bit1

added theorem gsmul_coe_nat

modified theorem gsmul_eq_mul'

modified theorem gsmul_eq_mul

added theorem gsmul_mul'

modified theorem gsmul_mul

deleted theorem gsmul_neg

deleted theorem gsmul_neg_one

added theorem gsmul_neg_succ

added theorem gsmul_of_nat

deleted theorem gsmul_one

modified theorem inv_gpow

modified theorem list.sum_repeat

modified theorem mul_gsmul_assoc

added theorem mul_gsmul_left

deleted theorem mul_gsmul_right

modified theorem nat.pow_eq_pow

added theorem neg_gsmul

added theorem neg_one_gsmul

modified theorem one_gpow

added theorem one_gsmul

modified theorem pow_abs

added theorem pow_mul'

modified theorem pow_mul_comm

modified theorem pow_zero

added theorem smul_add_comm'

added theorem smul_add_comm

deleted theorem smul_bit1

deleted theorem smul_succ'

deleted theorem smul_succ

deleted theorem smul_two

added theorem succ_smul'

added theorem succ_smul

added theorem two_smul

added theorem zero_gsmul

Modified analysis/limits.lean

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/topology/topological_space.lean

Modified data/int/basic.lean

modified theorem int.shiftl_eq_mul_pow

modified theorem int.shiftr_eq_div_pow

Modified data/multiset.lean

modified theorem multiset.count_smul

modified theorem multiset.prod_repeat

added theorem multiset.sum_map_sum_map

added theorem multiset.sum_repeat

Modified data/nat/sqrt.lean

Modified data/real/basic.lean

Modified data/set/lattice.lean

deleted theorem set.subset.antisymm_iff

Modified group_theory/subgroup.lean

modified theorem exists_gpow_eq_one

modified theorem exists_pow_eq_one

modified theorem gpow_eq_mod_order_of

modified theorem is_subgroup_range_gpow

modified theorem order_eq_card_range_gpow

modified theorem pow_eq_mod_order_of

modified theorem pow_order_of_eq_one

Modified leanpkg.toml

Modified linear_algebra/multivariate_polynomial.lean

Modified number_theory/pell.lean

Modified ring_theory/localization.lean

Modified set_theory/cardinal.lean

modified theorem cardinal.nat_cast_pow

Modified set_theory/ordinal.lean

modified theorem ordinal.nat_cast_power

Modified tactic/norm_num.lean

Modified tactic/ring.lean

Modified tests/norm_num.lean