Mathlib Changelog
v3
Changelog
About
Github
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