leanprover-community/mathlib

Pull Requests Commits

feat(order/filter/at_top_bot): add `at_bot` versions for (almost) all `at_top` lemmas (#3845)

ADedecker committed 5 years ago

67549d93

refactor(topology/metric_space/baire): use choose! in Baire theorem (#3852)

sgouezel committed 5 years ago

67e0019b

chore(data/set/finite): explicit `f` in `finset.preimage s f hf` (#3851)

urkud committed 5 years ago

65382743

feat(category_theory/abelian): pseudoelements and a four lemma (#3803)

TwoFX committed 5 years ago

c3561489

feat(algebra/ordered_*): cleanup and projection notation (#3850)

fpvandoorn committed 5 years ago

04948074

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

leanprover-community-bot committed 5 years ago

cd7c2287

chore(field_theory/tower): generalize tower law to modules (#3844)

kckennylau committed 5 years ago

b68702e6

feat(tactic/choose): derive local nonempty instances (#3842)

digama0 committed 5 years ago

3ea8e280

feat(ring_theory/localization): Generalize theorems about localization over an integral domain (#3780)

dtumad committed 5 years ago

f77530e9

feat(analysis/normed_space): generalize corollaries of Hahn-Banach (#3658)

Ruben-VandeVelde committed 5 years ago

f818acbe

fix(ring_theory/localization): remove coe_submodule instance (#3832)

digama0 committed 5 years ago

f8bf0016

feat(algebra): define linear recurrences and prove basic lemmas about them (#3829)

ADedecker committed 5 years ago

472251b0

feat(ring_theory/DVR,padics/padic_integers): characterize ideals of DVRs, apply to `Z_p` (#3827)

robertylewis committed 5 years ago

3edf2b27

feat(algebra/module): define ordered semimodules and generalize convexity of functions (#3728)

dupuisf committed 5 years ago

d4cb2372

refactor(logic/basic): classical -> root, root -> decidable (#3812)

digama0 committed 5 years ago

bc72d903

feat(lint): improved ge_or_gt linter (#3810)

fpvandoorn committed 5 years ago

1a8f6bf9

chore(analysis/normed_space/banach): correct typo (#3840)

sgouezel committed 5 years ago

2a8d7f3e

chore(analysis/hofer): use the new choose! (#3839)

PatrickMassot committed 5 years ago

41cbfdc3

feat(linear_algebra/affine_space/combination): centroid (#3825)

jsm28 committed 5 years ago

626de475

feat(category_theory): limits in the category of indexed families (#3737)

kim-em committed 5 years ago

6773f526

feat(geometry/euclidean): circumradius simp lemmas (#3834)

jsm28 committed 5 years ago

b0b5cd45

chore(data/nat/digits): refactor proof of `last_digit_ne_zero` (#3836)

shingtaklam1324 committed 5 years ago

43337f7e

fix(tactic/refine_struct): accept synonyms for `structure` types (#3828)

cipher1024 committed 5 years ago

c1fece37

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

leanprover-community-bot committed 5 years ago

56ed455a

feat(ring_theory/derivations): stab on derivations (#3688)

Nicknamen committed 5 years ago

40214fcb

feat(tactic/interactive/choose): nondependent choose (#3806)

digama0 committed 5 years ago

4f2c9585

chore(ring_theory/ideal): docstring for Krull's theorem and a special case (#3831)

TwoFX committed 5 years ago

3d4f085e

feat(analysis/special_functions/exp_log): `tendsto real.log at_top at_top` (#3826)

ADedecker committed 5 years ago

ee74e7f6

feat(data/padics): more valuations, facts about norms (#3790)

robertylewis committed 5 years ago

863bf793

feat(data/fin): bundled embedding (#3822)

jsm28 committed 5 years ago

a6f64343

Newer Older