leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'computability' of https://github.com/leanprover-community/mathlib into computability

MadPidgeon committed 5 years ago

8c36f73e

MadPidgeon committed 5 years ago

de00daa8

feat(algebraic_geometry): structure sheaf on Spec R (#3907)

kim-em committed 5 years ago

17c4651c

Fixed proof of encodek_nat

pimsp committed 5 years ago

80c5ca93

MadPidgeon committed 5 years ago

ec416a28

refactor(set_theory/game): make impartial a class (#3974)

TwoFX committed 5 years ago

84d47a0f

feat(analysis/convex): add correspondence between convex cones and ordered semimodules (#3931)

dupuisf committed 5 years ago

ea177c2a

chore(algebra/group_with_zero): adjust some instance priorities (#3968)

rwbarton committed 5 years ago

53275f49

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

leanprover-community-bot committed 5 years ago

2d3530d5

feat(linear_algebra): eigenspaces of linear maps (#3927)

abentkamp committed 5 years ago

4ccbb514

chore(group_theory/perm/sign): speed up proofs (#3963)

shingtaklam1324 committed 5 years ago

1353b7e7

doc(representation_theory/maschke): fix latex (#3965)

gebner committed 5 years ago

d77798a4

feat(category_theory/limits): add kernel pairs (#3925)

b-mehta committed 5 years ago

31db0bdd

feat(tactic/congr): additions to the congr' tactic (#3936)

fpvandoorn committed 5 years ago

a08fb2f7

feat(category_theory/filtered): filtered categories, and filtered colimits in `Type` (#3960)

kim-em committed 5 years ago

ceacf541

feat(topology/sheaves): checking the sheaf condition under a forgetful functor (#3609)

kim-em committed 5 years ago

513f7407

feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906)

kim-em committed 5 years ago

7e6393f8

feat(geometry/euclidean/basic): reflection (#3932)

jsm28 committed 5 years ago

eaaac992

feat(data/nat): commutativity of bitwise operations (#3956)

TwoFX committed 5 years ago

359261ef

feat(combinatorics/adjacency_matrix): defines adjacency matrices of simple graphs (#3672)

jalex-stark committed 5 years ago

6b556cf1

refactor(analysis/normed_space/real_inner_product,geometry/euclidean): orthogonal projection hypotheses (#3952)

jsm28 committed 5 years ago

ea9bf31e

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

leanprover-community-bot committed 5 years ago

5627aed7

feat(data/fin): flesh out API for fin (#3769)

pechersky committed 5 years ago

c1478948

feat(algebra/big_operators): sum of two products (#3944)

fpvandoorn committed 5 years ago

26dfea59

feat(category_theory/adjunction): uniqueness of adjunctions (#3940)

b-mehta committed 5 years ago

64aad5b8

feat(algebra/category/*/limits): don't rely on definitions (#3873)

kim-em committed 5 years ago

080746fd

feat(ring_theory/ideal/basic): R/I is an ID iff I is prime (#3951)

kbuzzard committed 5 years ago

2d9ab611

feat(topology/algebra/ordered): conditions for a strictly monotone function to be a homeomorphism (#3843)

hrmacbeth committed 5 years ago

2b6924d5

feat(ring_theory/bundled_subring): add bundled subrings (#3886)

kbuzzard committed 5 years ago

f4f0854c

feat(ring_theory/noetherian): maximal among set iff Noetherian (#3846)

jalex-stark committed 5 years ago

0d67a02d

Newer Older