leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into eric-wieser/decidable-linter

eric-wieser committed 4 years ago

Verified a67d2edb

chore(linear_algebra): switch to named constructors for linear_map (#8059)

eric-wieser committed 4 years ago

b9bf921c

chore(data/polynomial/eval, ring_theory/polynomial_algebra): golfs (#8058)

eric-wieser committed 4 years ago

2a1cabea

feat(data/matrix/basic.lean) : added map_scalar and linear_map.map_matrix (#8061)

faenuccio committed 4 years ago

5352639d

feat(analysis/liouville/liouville_constant): transcendental Liouville numbers exist! (#8020)

adomani committed 4 years ago

5bd649fb

feat(data/nat/prime): norm_num plugin for factors (#8009)

digama0 committed 4 years ago

f7f12bc6

feat(topology/topological_fiber_bundle): a new standard construction for topological fiber bundles (#7935)

Nicknamen committed 4 years ago

d9dcf699

refactor(algebra/ordered_monoid): use `covariant + contravariant` typeclasses in `algebra/ordered_monoid` (#7999)

adomani committed 4 years ago

2f27046f

feat(data/fin): some lemmas about casts (#8049)

ericrbg committed 4 years ago

56535164

chore(data/real/hyperreal): remove @ in a proof (#8063)

adomani committed 4 years ago

e07a24a1

chore(linear_algebra): deduplicate `linear_equiv.{Pi_congr_right,pi}` (#8056)

Vierkantor committed 4 years ago

b9ef710e

feat(measure_theory/set_integral): the set integral is continuous (#7931)

RemyDegenne committed 4 years ago

3cf80395

feat(category_theory/arrow/limit): limit cones in arrow categories (#7457)

jcommelin committed 4 years ago

a31e3c3c

docs(data/fin2): add module docstring (#8047)

YaelDillies committed 4 years ago

204ca5f9

docs(data/option/defs): add module and def docstrings (#8042)

YaelDillies committed 4 years ago

89b8e0b2

docs(data/list/bag_inter): add module docstring (#8034)

YaelDillies committed 4 years ago

431207ae

feat(analysis/normed_space/basic): add has_nnnorm (#7986)

riccardobrasca committed 4 years ago

dd5074c4

feat(category_theory/arrow): arrow.iso_mk (#8057)

jcommelin committed 4 years ago

a7b5237d

docs(data/list/tfae): add module docstring (#8040)

YaelDillies committed 4 years ago

c841b09a

docs(data/list/zip): add module docstring (#8036)

YaelDillies committed 4 years ago

5787d64b

docs(data/list/forall2): add module docstring (#8029)

YaelDillies committed 4 years ago

97529b4c

feat(analysis/liouville/inequalities_and_series): two useful inequalities for Liouville (#8001)

adomani committed 4 years ago

d9eed422

feat(algebra/ordered_monoid_lemmas + fixes): consistent use of `covariant` and `contravariant` in `ordered_monoid_lemmas` (#7876)

adomani committed 4 years ago

47ed97f3

feat(analysis/liouville/liouville_constant): develop some API for Liouville (#8005)

adomani committed 4 years ago

168678ed

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

leanprover-community-bot committed 4 years ago

ac2142c0

feat(algebra/ordered_field): a few monotonicity results for powers (#8022)

adomani committed 4 years ago

0bc09d9a

chore(topology/basic): add missing lemma (#8048)

adamtopaz committed 4 years ago

949e98e6

feat(ring_theory/adjoin/basic): lemmas relating adjoin and submodule.span (#8031)

hrmacbeth committed 4 years ago

de4a4ce1

chore(topology/continuous_function/algebra): delete old instances, use bundled sub[monoid, group, ring]s (#8004)

ADedecker committed 4 years ago

c594196f

feat(analysis/normed_space/multilinear): add a few inequalities (#8018)

urkud committed 4 years ago

83bd2e68

Older