Commits leanprover-community/mathlib3

chore(algebra/hom): add `inline` attributes to preserve computability

eric-wieser committed 3 years ago

68a79da1

feat(probability_theory/independence): if a family of pi-systems is independent, then so are the generated measurable spaces (#9387)

RemyDegenne committed 3 years ago

3594b635

feat(measure_theory/function/lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999)

kex-y committed 3 years ago

728e074e

feat(order/symm_diff): Triangle inequality for the symmetric difference (#14847)

YaelDillies committed 3 years ago

dcedc047

chore(topology/uniform_space/basic): Make `to_topological_space_inf` and `inf_uniformity` true by definition (#14912)

eric-wieser committed 3 years ago

ae3d5722

chore(analysis/special_functions/trigonometric/angle): rfl lemmas for nat and int smul actions on angle (#15003)

eric-wieser committed 3 years ago

cf4d987d

chore(topology/separation): Extract `set` product lemma (#14958)

YaelDillies committed 3 years ago

37bf8a2e

chore(data/set/basic): remove duplicate `nonempty_insert` in favor of `insert_nonempty` (#14884)

vihdzp committed 3 years ago

ee7f38c7

feat(data/bool): bnot_ne (#10562)

rgreenblatt committed 3 years ago

365b2ee5

feat(data/finset/pointwise): `•` and `⊆` (#14968)

YaelDillies committed 3 years ago

f6b728f4

chore(set_theory/game/pgame): remove weird `simp` lemma (#14954)

vihdzp committed 3 years ago

7c6cd38b

feat(data/multiset/basic): add multiset.filter_singleton (#14938)

BoltonBailey committed 3 years ago

2cdded92

chore(data/nat/factorization/basic): golf pow_succ_factorization_not_dvd, remove import (#14936)

stuart-presnell committed 3 years ago

927b4685

feat(analysis/locally_convex/bounded): continuous linear image of bounded set is bounded (#14907)

ADedecker committed 3 years ago

f51286dd

chore(algebra/group/units): mark some lemmas as simp (#14871)

alexjbest committed 3 years ago

cf50ac12

feat(set_theory/cardinal/basic): lemmas about `#(finset α)` (#14850)

vihdzp committed 3 years ago

cad1a6c6

refactor(topology/inseparable): redefine `specializes` and `inseparable` (#14647)

urkud committed 3 years ago

fef4fb83

feat(analysis/special_functions/log/deriv): more power series for log (#14881)

mo271 committed 3 years ago

1cd2bf58

chore(data/int/cast): redo #14890, moving field-specific lemmas (#14995)

Vierkantor committed 3 years ago

68e01601

feat(*): Upgrade to lean 3.44.1c (#14984)

eric-wieser committed 3 years ago

2558b3b3

doc(analysis/convex/uniform_convex_space): End of sentence (#14986)

YaelDillies committed 3 years ago

05565f4d

feat(order/*): Miscellaneous results about the product order (#14977)

YaelDillies committed 3 years ago

5de7c346

feat(measure_theory/function/l1_space): add some integrability lemmas (#14931)

kex-y committed 3 years ago

f5d2cc8f

feat(analysis/convex/special_functions): `sqrt * log` is strictly convex on x>1 (#14822)

tb65536 committed 3 years ago

cf8b46d7

feat(probability/stopping): measurability of sets related to stopping times, under countable/encodable assumptions (#14750)

RemyDegenne committed 3 years ago

68d29f52

feat(probability/moments): moments and moment generating function of a real random variable (#14755)

RemyDegenne committed 3 years ago

331df5a2

feat(probability/stopping): if a filtration is sigma finite, then the measure restricted to the sigma algebra generated by a stopping time is sigma finite (#14752)

RemyDegenne committed 3 years ago

3091b91e

feat(measure_theory/measure/finite_measure_weak_convergence): Characterize weak convergence of finite measures in terms of integrals of bounded continuous real-valued functions. (#14578)

kkytola committed 3 years ago

72fbe5c3

chore(data/sigma/basic): make `sigma.reflect` universe-polymorphic (#14934)

eric-wieser committed 3 years ago

cf0649c5

chore(algebra/direct_sum/ring): add new `int_cast` and `nat_cast` fields to match `ring` and `semiring` (#14976)

eric-wieser committed 3 years ago

671c7c05