leanprover-community/mathlib

Pull Requests Commits

erdOne committed 4 years ago

69423535

Merge branch 'dense_subsite' into cover_preserving_and_lifting

erdOne committed 4 years ago

531210a1

erdOne committed 4 years ago

0737c9e6

erdOne committed 4 years ago

31acea6b

erdOne committed 4 years ago

457e979e

erdOne committed 4 years ago

817f5437

stopped fixing stuff

erdOne committed 4 years ago

5c13c920

finished `iso_of_restrict_iso`

erdOne committed 4 years ago

365e8b57

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

leanprover-community-bot committed 4 years ago

ea70e1c0

chore(data/sym/sym2): speed up some proofs (#9677)

Ruben-VandeVelde committed 4 years ago

c65de1e6

feat(topology/instances/ennreal): if a tsum is finite, then the tsum over the complement of a finset tends to 0 at top (#9665)

sgouezel committed 4 years ago

66285c9f

feat(category_theory/*): Functors about comma categories. (#9627)

erdOne committed 4 years ago

817c70db

feat(algebra/star/basic): add some helper lemmas about star (#9651)

eric-wieser committed 4 years ago

f63b8f12

chore(analysis): fix file name (#9673)

PatrickMassot committed 4 years ago

b486c88f

chore(set_theory/cardinal): move defs/lemmas about `lift` up (#9669)

urkud committed 4 years ago

bcb29439

feat(order/filter): `∃ᶠ m in at_top, m ≡ d [MOD n]` (#9666)

urkud committed 4 years ago

a979d15c

refactor(combinatorics/partition): add `nat` namespace (#9672)

YaelDillies committed 4 years ago

fd7da4ef

refactor(data/opposite): Remove the `op_induction` tactic (#9660)

eric-wieser committed 4 years ago

2e72f352

feat(algebra/opposites): provide npow and gpow explicitly, prove `op_gpow` and `unop_gpow` (#9659)

eric-wieser committed 4 years ago

ad4040dd

feat(linear_algebra/affine_space/finite_dimensional): upgrade `affine_independent.affine_span_eq_top_of_card_eq_finrank_add_one` to an iff (#9657)

ocfnash committed 4 years ago

34ffb154

chore(ring_theory/tensor_product): squeeze simps in a slow proof (#9671)

sgouezel committed 4 years ago

1023d812

chore(analysis): move some files to `analysis/normed/group` (#9667)

urkud committed 4 years ago

a132d0ab

feat(data/dfinsupp, algebra/direct_sum/module): direct sum on fintype (#9664)

hrmacbeth committed 4 years ago

638dd0f8

feat(analysis/normed_space/normed_group_hom): add norm_noninc.neg (#9658)

riccardobrasca committed 4 years ago

c2a30bef

feat(topology/path_connected): add `path.reparam` for reparametrising a path. (#9643)

shingtaklam1324 committed 4 years ago

df132fe6

feat(topology/homotopy/path): Add homotopy between paths (#9141)

shingtaklam1324 committed 4 years ago

136d0ce9

feat(analysis/normed/group/basic): add norm_le_add_norm_add (#9655)

riccardobrasca committed 4 years ago

6872dfb5

feat(tactic/lint/misc): unused haves and suffices linters (#9310)

alexjbest committed 4 years ago

fa5d9d61

erdOne committed 4 years ago

7451cde7

feat(number_theory/liouville): Liouville numbers form a dense Gδ set (#9646)

urkud committed 4 years ago

c2fde701

Older