leanprover-community/mathlib

Pull Requests Commits

chore(combinatorics/choose/bounds): move to nat namespace (#10106)

eric-wieser committed 4 years ago

6df3143a

style(testing/slim_check): fix line length (#10114)

PatrickMassot committed 4 years ago

0dcb1849

feat(measure_theory/decomposition/lebesgue): more on Radon-Nikodym derivatives (#10070)

sgouezel committed 4 years ago

796a051a

feat(data/mv_polynomial/basic): lemmas about map (#10092)

eric-wieser committed 4 years ago

da6706d0

refactor(order/bounded_lattice): generalize le on with_{top,bot} (#10085)

pechersky committed 4 years ago

80dc445d

refactor(algebra/algebra): remove subalgebra.under (#10081)

eric-wieser committed 4 years ago

658a3d77

feat(topology/algebra/ordered/liminf_limsup): convergence of a sequence which does not oscillate infinitely (#10073)

sgouezel committed 4 years ago

541df8a0

chore(analysis/normed/group): add `cauchy_seq_finset_of_norm_bounded_eventually` (#10060)

urkud committed 4 years ago

880182d6

feat(measure_theory/probability_mass_function): Define uniform pmf on an inhabited fintype (#9920)

dtumad committed 4 years ago

fc12ca8d

chore(ring_theory/adjoin/fg): generalize ring to semiring in a few places (#10089)

eric-wieser committed 4 years ago

f6894c47

chore(coinductive_predicates): remove private and use of import_private (#10084)

kim-em committed 4 years ago

26bdcac0

feat(analysis/calculus/mean_value): Strict convexity from derivatives (#10034)

YaelDillies committed 4 years ago

18528404

chore(data/list/defs): remove unneeded open (#10100)

kim-em committed 4 years ago

6d2af9a1

chore(scripts): update nolints.txt (#10098)

leanprover-community-bot committed 4 years ago

d926ac73

chore(algebra/free_algebra): remove a heavy and unecessary import (#10093)

eric-wieser committed 4 years ago

fd783e39

chore(analysis/normed_space/operator_norm): remove an import to data.equiv.transfer_instance (#10094)

eric-wieser committed 4 years ago

b1d5446e

chore({data/finset,data/multiset,order}/locally_finite): Better line wraps (#10087)

YaelDillies committed 4 years ago

0144b6ca

chore(category_theory/limits): reuse a previous result (#10088)

TwoFX committed 4 years ago

fef1535b

chore(algebra/algebra): implement subalgebra.under in terms of restrict_scalars (#10080)

eric-wieser committed 4 years ago

9ef310f2

chore(ring_theory/algebra_tower): relax typeclasses (#10078)

eric-wieser committed 4 years ago

17ebcf01

chore(analysis/normed_space/operator_norm): semilinearize part of the file (#10076)

dupuisf committed 4 years ago

23892a05

feat(algebra/direct_sum/module) : coe and internal (#10004)

jjaassoonn committed 4 years ago

85fe90e9

docs(category_theory/*): add missing module docs (#9990)

kim-em committed 4 years ago

acc504e1

chore(scripts): update nolints.txt (#10083)

leanprover-community-bot committed 4 years ago

e8fa2328

fix(data/{rbtree,rbmap}): fix some lint errors (#10036)

urkud committed 4 years ago

cd457a5d

feat(algebra/direct_sum/basic): some lemmas about `direct_sum.of` (#10003)

jjaassoonn committed 4 years ago

bf821223

feat(data/finset): some simple finset lemmas (#10079)

b-mehta committed 4 years ago

932e9548

feat(data/list): length_filter_lt_length_iff_exists (#10074)

TwoFX committed 4 years ago

60cb2cfe

feat(list/init): simplifier lemmas for list.init (#10061)

EPronovost committed 4 years ago

af4f4df5

chore(data/list/basic): use dot notation here and there (#10056)

urkud committed 4 years ago

d6dd4516

Newer Older