Commits leanprover-community/mathlib3

feat(data/nat/factorization): Defining `factorization` (#10540)

stuart-presnell committed 4 years ago

a8d37c1d

feat(topology/homotopy/equiv): Add homotopy equivalences between topological spaces (#10529)

shingtaklam1324 committed 4 years ago

3b02ad77

feat(algebra,linear_algebra,ring_theory): more is_central_scalar instances (#11297)

eric-wieser committed 4 years ago

13e99c70

chore(category_theory/abelian/basic): abelian categories have finite limits and finite colimits. (#11271)

adamtopaz committed 4 years ago

b8f5d0ac

chore(topology/algebra/module/basic): add continuous_linear_map.is_central_scalar (#11291)

eric-wieser committed 4 years ago

b4303168

feat(topology/*): Gluing topological spaces (#9864)

erdOne committed 4 years ago

3b7a783f

feat(*): add lemmas, golf (#11294)

urkud committed 4 years ago

6fb638b3

feat(algebra/{monoid_algebra/basic,free_non_unital_non_assoc_algebra,lie/free}): generalize typeclasses (#11283)

eric-wieser committed 4 years ago

0b966303

feat(set_theory/ordinal): `ordinal` is a successor order (#11284)

YaelDillies committed 4 years ago

d0bf8bd2

feat(data/polynomial/monic): add two lemmas on degrees of monic polynomials (#11259)

adomani committed 4 years ago

5893fbfc

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