leanprover-community/mathlib

Pull Requests Commits

Cleaner line breaks.

kkytola committed 3 years ago

c0e5d603

Small docstring edits.

kkytola committed 3 years ago

839a8e8e

Merge branch 'master' into kkytola/tendsto_indicator_thickening

kkytola committed 3 years ago

ce3a99e2

Change also the final lemmas to mul_indicator form with to_additive attributes.

kkytola committed 3 years ago

2b46eea7

Move two lemmas to hausdorff_distance.lean.

kkytola committed 3 years ago

ed269dd5

A better organization of the proof.

kkytola committed 3 years ago

24394e60

Generalize as suggested.

kkytola committed 3 years ago

4eceb5e4

feat(logic/denumerable): Any two infinite countable types are equivalent (#17903)

YaelDillies committed 3 years ago

fc2ed6f8

feat(number_theory/modular_forms): Modular form definition (#13250)

AlexKontorovich committed 3 years ago

32d096dc

feat(linear_algebra/affine_space/independent): spans of two affine combinations (#17861)

jsm28 committed 3 years ago

ee00ca5e

feat(data/set/basic): A set is either a subsingleton or nontrivial (#17901)

YaelDillies committed 3 years ago

bd59f822

refactor(linear_algebra/basic): use `bijective` in `linear_equiv.of_bijective` (#17897)

eric-wieser committed 3 years ago

6d584f17

fix(analysis/normed_space/basic): add back computable module instance (#17813)

eric-wieser committed 3 years ago

85158adc

feat(analysis/convex/cone/basic): submodules are convex cones (#17749)

eric-wieser committed 3 years ago

800f5229

feat(topology): `zero_at_infty_continuous_map`s are `uniform_continuous` (#17767)

alreadydone committed 3 years ago

1c521b4f

feat(data/list/basic): add lemma map_eq_repeat_iff (#17832)

MichaelStollBayreuth committed 3 years ago

cf9386b5

feat(group_theory/perm/basic): `subtype_perm` is a monoid hom (#17816)

YaelDillies committed 3 years ago

4f4e7fa6

chore(data/list/range): split & reduce imports (#17887)

astrainfinita committed 3 years ago

9925a115

refactor(topology/algebra/ring): rename subring.subring_topological_closure to subring.le_topological_closure (#17649)

xroblot committed 3 years ago

43afc5ad

feat(algebra/module/big_operators): Product of sums (#17818)

YaelDillies committed 3 years ago

4e87c847

chore(data/multiset/nodup): remove dependency on `multiset.powerset` (#17888)

astrainfinita committed 3 years ago

036348ae

refactor(algebra/group/defs): use `is_left_cancel_mul` etc (#17884)

urkud committed 3 years ago

2e0975f6

chore(data/finset): remove unused imports (#17891)

astrainfinita committed 3 years ago

955890d3

chore(number_theory/ramification_inertia): make an argument explicit (#17890)

eric-wieser committed 3 years ago

68f41d3c

chore(number_theory/padics/padic_val): golf (#17885)

urkud committed 3 years ago

60fa54e7

chore(*): add mathlib4 synchronization comments (#17871)

github-actions[bot] committed 3 years ago

eedb2810

feat(algebraic_topology/dold-kan): The Dold-Kan equivalence for additive categories (#17640)

joelriou committed 3 years ago

19d6240d

feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime (#17877)

riccardobrasca committed 3 years ago

12d63a7f

refactor(topology/instances/add_circle): redefine `equiv_add_circle` (#17881)

urkud committed 3 years ago

f178c0e2

feat(linear_algebra/basic): add linear_map.eq_locus (#17751)

eric-wieser committed 3 years ago

f1d5b468

Older