leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/binary_products): some product lemmas and their dual (#2752)

b-mehta committed 5 years ago

ab5d0f15

docs(linear_algebra/sesquilinear_form): correct module docs (#2757)

Vierkantor committed 5 years ago

1f002829

feat(linear_algebra/projection): projection to a subspace (#2739)

urkud committed 5 years ago

cbe80ed2

feat(data/nat/choose): sum_range_choose_halfway (#2688)

Smaug123 committed 5 years ago

3c1f9f9c

feat(logic/basic): spaces with a zero or a one are nonempty (#2743)

sgouezel committed 5 years ago

e3aca90a

feat(algebra/big_operators): reversing an interval doesn't change the product (#2740)

urkud committed 5 years ago

607767e2

fix(ci): replace 2 old secret names (#2744)

bryangingechen committed 5 years ago

62c22daf

chore(*): remove non-canonical `option.decidable_eq_none` instance (#2741)

gebner committed 5 years ago

1e185125

fix(*): put headings in multiline module docs on their own lines (#2742)

bryangingechen committed 5 years ago

93b41e56

feat(analysis/normed_space): interior of `closed_ball` etc (#2723)

urkud committed 5 years ago

3d948bf1

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

bryangingechen committed 5 years ago

f2cb5462

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

TwoFX committed 5 years ago

3968f7f4

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

robertylewis committed 5 years ago

80b7f975

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

jcommelin committed 5 years ago

3ba7d128

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

TwoFX committed 5 years ago

52aa1281

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

urkud committed 5 years ago

906220ca

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

robertylewis committed 5 years ago

01efaebc

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

jcommelin committed 5 years ago

f01260a7

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

leanprover-community-bot committed 5 years ago

9d762df7

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

rwbarton committed 5 years ago

ff3130da

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

rwbarton committed 5 years ago

4026bd8c

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

rwbarton committed 5 years ago

2fa1d7cd

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

jcommelin committed 5 years ago

8b422458

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

Smaug123 committed 5 years ago

18217e9a

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

gebner committed 5 years ago

434e6a65

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

leanprover-community-bot committed 5 years ago

93119dd6

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

robertylewis committed 5 years ago

73251047

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

jcommelin committed 5 years ago

cdf97dcc

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

jcommelin committed 5 years ago

f23c361e

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

Smaug123 committed 5 years ago

3449510c

Older