leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/*/pi): add missing lemmas about function.update and set.piecewise (#9935)

eric-wieser committed 4 years ago

942e60f7

docs(control/bitraversable/instances): Add def docstrings (#9931)

YaelDillies committed 4 years ago

1e7f6b9a

docs(control/applicative): Add module docstring (#9930)

YaelDillies committed 4 years ago

5d1e8f79

docs(control/bitraversable/basic): Add defs docstrings (#9929)

YaelDillies committed 4 years ago

6f1d45dc

docs(control/traversable/equiv): Add module docstring (#9928)

YaelDillies committed 4 years ago

5642c628

feat(group_theory/subgroup/basic): Contrapositive of `card_le_one_iff_eq_bot` (#9918)

tb65536 committed 4 years ago

8c0b8c71

feat(data/nat/log): Equivalent conditions for logarithms to equal zero and one (#9903)

Smaug123 committed 4 years ago

44682319

feat(data/list): product of list.update_nth in terms of inverses (#9800)

dtumad committed 4 years ago

12515db6

feat(dynamics/ergodic/measure_preserving): add `measure_preserving.symm` (#9940)

urkud committed 4 years ago

c20f08ed

feat(measure_theory/integral): Divergence theorem for Bochner integral (#9811)

urkud committed 4 years ago

4ea8de91

split(analysis/normed_space/exponential): split file to minimize dependencies (#9932)

ADedecker committed 4 years ago

a30e1900

feat(topology): add some lemmas (#9907)

fpvandoorn committed 4 years ago

dc6b8e1c

split(data/list/lattice): split off `data.list.basic` (#9906)

YaelDillies committed 4 years ago

696f07f2

feat(topology/algebra/group): continuous div lemmas (#9905)

fpvandoorn committed 4 years ago

9dc3b4d6

feat(data/real/nnreal): use the nonneg instance (#9701)

fpvandoorn committed 4 years ago

be948000

feat(analysis/normed_space/is_R_or_C): add three lemmas on bounds of linear maps over is_R_or_C. (#9827)

kkytola committed 4 years ago

416edeed

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

leanprover-community-bot committed 4 years ago

ecc544ea

feat(order/galois_connection): add `exists_eq_{l,u}`, tidy up lemmas (#9904)

eric-wieser committed 4 years ago

e836a722

chore(topology): generalize `real.image_Icc` etc (#9784)

urkud committed 4 years ago

49c68412

feat(linear_algebra): add notation for star-linear maps (#9875)

hrmacbeth committed 4 years ago

55a11604

feat(nat/choose/central): definition of the central binomial coefficient, and bounds (#9753)

Smaug123 committed 4 years ago

5ec1572c

feat(ring_theory): generalize `adjoin_root.power_basis` (#9536)

Vierkantor committed 4 years ago

d788647f

docs(data/dlist/instances): Add module docstring (#9912)

YaelDillies committed 4 years ago

928d0e03

docs(data/list/sigma): Add missing def dosctrings, expand module docs (#9909)

YaelDillies committed 4 years ago

15161e96

refactor(analysis/special_functions/exp_log): split into 4 files (#9882)

urkud committed 4 years ago

75b1a94a

feat(topology/metric_space/lipschitz): continuity on product of continuity in 1 var and Lipschitz continuity in another (#9758)

urkud committed 4 years ago

59db9032

docs(control/traversable/instances): Add module docstring (#9913)

YaelDillies committed 4 years ago

939e8b9a

docs(control/bifunctor): Add module and defs docstrings (#9911)

YaelDillies committed 4 years ago

14b998b2

chore(data/real/sqrt): A couple of lemmas about sqrt (#9892)

Smaug123 committed 4 years ago

78252a30

feat(linear_algebra/free_module/pid): golf basis.card_le_card_of_linear_independent_aux (#9813)

riccardobrasca committed 4 years ago

3f58dc78

Newer Older