leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into replace_conj_with_star

eric-wieser committed 4 years ago

e50c5c5f

feat(algebra/star): `star_gpow` and `star_fpow` (#9661)

eric-wieser committed 4 years ago

2c8abe52

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

Merge branch 'master' into replace_conj_with_star

dupuisf committed 4 years ago

09389152

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

Merge branch 'master' into replace_conj_with_star

dupuisf committed 4 years ago

893fef1d

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

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

urkud committed 4 years ago

c2fde701

feat(data/finset): add `finset.erase_none` (#9630)

urkud committed 4 years ago

082aa832

refactor(topology/sheaves/*): Make sheaf condition a Prop (#9607)

justus-springer committed 4 years ago

1539ee18

feat(algebra.algebra.subalgebra): add `subalgebra.gc_map_comap` (#9435)

urkud committed 4 years ago

4a191ad9

feat(group_theory/subgroup/basic): apply_mem_map_injective (#9637)

tb65536 committed 4 years ago

30cf8b77

feat(algebra/floor): When the floor is strictly positive (#9625)

YaelDillies committed 4 years ago

957f64ee

Older