leanprover-community/mathlib3

Pull Requests Commits

fix(ci): setup git before nolints, rename secret (#2737)

bryangingechen committed 6 years ago

f2cb5462

feat(linear_algebra): equiv_of_is_basis' and module.fintype_of_fintype (#2735)

TwoFX committed 6 years ago

3968f7f4

feat(tactic/localized): fail if unused locale is open (#2718)

robertylewis committed 6 years ago

80b7f975

feat(algebra): obtaining algebraic classes through in/surjective maps (#2638)

jcommelin committed 6 years ago

3ba7d128

feat(data/equiv): add add_equiv.to_multiplicative (#2732)

TwoFX committed 6 years ago

52aa1281

feat(topology/bounded_continuous_function): Normed algebra of bounded continuous functions (#2722)

urkud committed 6 years ago

906220ca

feat(ci): run lint and tests in parallel (#2736)

robertylewis committed 6 years ago

01efaebc

feat(algebra/char_p): eq_iff_modeq_int (#2731)

jcommelin committed 6 years ago

f01260a7

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

leanprover-community-bot committed 6 years ago

9d762df7

feat(topology/constructions): topology on ulift (#2716)

rwbarton committed 6 years ago

ff3130da

feat(category_theory/full_subcategory): induced category from a groupoid is a groupoid (#2715)

rwbarton committed 6 years ago

4026bd8c

Revert "fix(category_theory/eq_to_hom): remove bad simp lemmas (#1346)" (#2713)

rwbarton committed 6 years ago

2fa1d7cd

refactor(algebra): merge init_.algebra into algebra (#2707)

jcommelin committed 6 years ago

8b422458

feat(nat/choose): Generalise nat.dvd_choose (#2703)

Smaug123 committed 6 years ago

18217e9a

chore(*): update to lean 3.13.2 (#2728)

gebner committed 6 years ago

434e6a65

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

leanprover-community-bot committed 6 years ago

93119dd6

feat(ci): store xz archives (#2719)

robertylewis committed 6 years ago

73251047

refactor(field_theory): preparations for Chevalley–Warning (#2590)

jcommelin committed 6 years ago

cdf97dcc

chore(*): bump to lean-3.13.1 (#2697)

jcommelin committed 6 years ago

f23c361e

feat(algebra/big_operators): Alternative phrasing of prod-bij (#2709)

Smaug123 committed 6 years ago

3449510c

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

leanprover-community-bot committed 6 years ago

a206df1e

refactor(normed_space): require `norm_smul_le` instead of `norm_smul` (#2693)

urkud committed 6 years ago

b530cdb4

chore(algebra/ring): drop an unneeded instance (#2705)

urkud committed 6 years ago

39af0f66

fix(algebra/big_operators): typo fix (#2704)

jsm28 committed 6 years ago

1580cd87

feat(archive/100-theorems-list): Sum of the Reciprocals of the Triangular Numbers (#2692)

jalex-stark committed 6 years ago

4f484a1e

feat(ring_theory/ideal_operations): jacobson radical, is_local, and primary ideals (#768)

kckennylau committed 6 years ago

21bdb787

refactor(group_theory/monoid_localization): use old_structure_cmd (#2683)

101damnations committed 6 years ago

00024db7

feat(data/finset): remove uses of choice for infima (#2699)

b-mehta committed 6 years ago

a7b17cdd

feat(data/finset) Another finset disjointness lemma (#2698)

Smaug123 committed 6 years ago

c81be77b

doc(tactic/solve_by_elim): improve docs (#2696)

kim-em committed 6 years ago

4b71428d

Newer Older