leanprover-community/mathlib3

Pull Requests Commits

do we want to change these lemmas?

fpvandoorn committed 4 years ago

fc6d5dab

fpvandoorn committed 4 years ago

a4a08da5

fpvandoorn committed 4 years ago

f5b87b80

feat(algebra/group/freiman): Freiman homomorphisms (#10497)

YaelDillies committed 4 years ago

9b39ab2a

feat(ring_theory/localization): Localization is the localization of localization. (#11145)

erdOne committed 4 years ago

d2428fae

feat(category_theory/sites): The pushforward pullback adjunction (#11273)

erdOne committed 4 years ago

54c2567d

feat(algebra/big_operators/multiset): Multiset product under some usual maps (#10907)

YaelDillies committed 4 years ago

7af5e86c

feat(topology/metric_space/kuratowski): make the Kuratowski embedding have codomain the "true" ℓ^∞(ℕ) (#11280)

hrmacbeth committed 4 years ago

c391512e

feat(ring_theory/power_series/basic): algebra, solving TODOs (#11267)

pechersky committed 4 years ago

f07f87e9

feat(data/nat/digits): digits_len (#11187)

pechersky committed 4 years ago

69521729

feat(measure_theory/constructions/borel_space): new lemma tendsto_measure_cthickening (#11009)

sgouezel committed 4 years ago

b3260f37

chore(ci): update some workflows to use custom bot token (#11274)

robertylewis committed 4 years ago

9f28b5d4

feat(topology/uniform_space/compact_convergence): when the domain is compact, compact convergence is just uniform convergence (#11262)

ocfnash committed 4 years ago

e7189651

chore(*): notation for `units` (#11236)

jcommelin committed 4 years ago

a7611b2c

feat(set_theory/ordinal_arithmetic): Proved characterization of `log` (#11192)

vihdzp committed 4 years ago

cac4e196

refactor(set_theory/ordinal_arithmetic): Reworked `sup` and `bsup` API (#11048)

vihdzp committed 4 years ago

b67857e7

feat(analysis/normed_space/lp_space): completeness of the lp space on `Π i, E i` (#11094)

hrmacbeth committed 4 years ago

771d1449

feat(ring_theory/laurent_series): laurent_series is_fraction_ring over power_series (#11220)

pechersky committed 4 years ago

8b2d1815

feat(measure_theory/integral): Cauchy integral formula for a circle (#10000)

urkud committed 4 years ago

f6dfea67

doc(analysis/normed/group/basic): show notation in the typeclass docstring (#11260)

eric-wieser committed 4 years ago

6bf90418

feat(algebra/polynomial/big_operators): lemmas about polynomial degree of products (#11258)

alexjbest committed 4 years ago

3ab1c1cb

chore(topology): move 3 files to `topology/algebra/module/` (#11242)

urkud committed 4 years ago

a1f4ac35

feat(category_theory/sites/left_exact): Sheafification is left exact. (#11252)

adamtopaz committed 4 years ago

9fd7a02d

chore(topology/omega_complete_partial_order): golf (#11250)

urkud committed 4 years ago

a5807271

feat(data/fintype/basic): `set_fintype_card_eq_univ_iff` (#11244)

tb65536 committed 4 years ago

802f23cf

feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_product}_cons` (#11241)

eric-wieser committed 4 years ago

b27e33a0

feat(linear_algebra/orientation): bases from orientations (#11234)

jsm28 committed 4 years ago

98b64f49

feat(analysis/complex): `re`, `im`, and `closure`/`interior`/`frontier` (#11215)

urkud committed 4 years ago

33b5d264

feat(ring_theory/non_zero_divisors): mul_{left,right}_cancel API (#11211)

pechersky committed 4 years ago

3115ced1

chore(data/nat/prime): reuse a result from algebra.big_operators.associated (#11143)

Ruben-VandeVelde committed 4 years ago

3bd2044b

Older