leanprover-community/mathlib

Pull Requests Commits

b-mehta committed 4 years ago

Verified f92a4221

b-mehta committed 4 years ago

Verified c27070e3

b-mehta committed 4 years ago

Verified c3ee6108

attempt set_like

b-mehta committed 4 years ago

Verified a907d23a

Merge branch 'master' into GeoLean

b-mehta committed 4 years ago

Verified 0df4e6ef

feat(data/nat/prime): Add lemma `factors_count_pow` (#10554)

stuart-presnell committed 4 years ago

cc604706

feat(analysis/normed_space/star and data/complex/is_R_or_C): register instances of `cstar_ring` (#10555)

j-loreaux committed 4 years ago

599a5118

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

leanprover-community-bot committed 4 years ago

3f7d0cfd

chore(analysis/mean_inequalities[_pow]): use vector notation (#10546)

hrmacbeth committed 4 years ago

49f8b6b8

feat(algebra/char_p/two): couple more lemmas + 🏌️ (#10467)

eric-wieser committed 4 years ago

b876e76b

doc(data/stream/defs): add docstrings to most defs (#10547)

urkud committed 4 years ago

cd69351b

refactor(algebra/group/basic): Migrate `add_group` section into `group` section (#10532)

mans0954 committed 4 years ago

8bce7eb0

feat(data/nat/pairing): add an `equiv` version of `nat.mkpair`/`nat.unpair` (#10520)

urkud committed 4 years ago

41fa32b3

feat(topology/[continuous_function, path_connected]): add bundled versions of prod_mk and prod_map (#10512)

ADedecker committed 4 years ago

af5c778c

feat(topology/connected): Connectedness in sum and sigma type (#10511)

YaelDillies committed 4 years ago

4d90ff97

feat(linear_algebra/affine_space/basis): upgrade `affine_basis.coords` to an affine map (#10452)

ocfnash committed 4 years ago

73562699

fix(*): replace "the the" by "the" (#10548)

jcommelin committed 4 years ago

35574bbf

feat(algebraic_geometry): Generalized basic open for arbitrary sections (#10515)

erdOne committed 4 years ago

1077f346

feat(group_theory/submonoid/pointwise): pointwise inverse of a submonoid (#10451)

eric-wieser committed 4 years ago

6102d771

feat(analysis/normed_space/spectrum and algebra/algebra/spectrum): prove properties of spectrum in a Banach algebra (#10530)

j-loreaux committed 4 years ago

4a9aa275

feat(category_theory/sites/compatible_*): Compatibility of plus and sheafification with composition. (#10510)

adamtopaz committed 4 years ago

f11d505e

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

leanprover-community-bot committed 4 years ago

396351bd

feat(algebra/char_p/two): lemmas about characteristic two (#10442)

eric-wieser committed 4 years ago

04fc415a

refactor(order/filter/bases): drop `p` in `has_antitone_basis` (#10499)

urkud committed 4 years ago

f798f22e

chore(order): fix-ups after #9891 (#10538)

pechersky committed 4 years ago

da6aceb8

chore(logic/function): allow `Sort*` in `function.inv_fun` (#10526)

urkud committed 4 years ago

7545909c

chore(data/stream): dedup `take` and `approx` (#10525)

urkud committed 4 years ago

3ac9ae73

chore(*): cleanup unneeded uses of by_cases across the library (#10523)

alexjbest committed 4 years ago

bc4ed5c0

chore(*): a few facts about `pprod` (#10519)

urkud committed 4 years ago

56018332

refactor(algebra.order.group): Convert abs_eq_sup_neg to multiplicative form (#10505)

mans0954 committed 4 years ago

be48f958

Older