leanprover-community/mathlib3

Pull Requests Commits

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

feat(set/basic): additions to prod (#3943)

fpvandoorn committed 5 years ago

187bfa52

feat(*/category/*): add coe_of simp lemmas (#3938)

kim-em committed 5 years ago

fb6046ed

chore(*): trivial golfing using dec_trivial tactic (#3949)

jcommelin committed 5 years ago

206673e7

feat(finsupp/basic): add hom_ext (#3941)

kbuzzard committed 5 years ago

dd742dc8

fix(set_theory/game): remove stray #lint introduced in #3939 (#3948)

TwoFX committed 5 years ago

a31096de

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

leanprover-community-bot committed 5 years ago

da475484

feat(algebra/group/with_one): more API for with_zero (#3716)

kbuzzard committed 5 years ago

666a2e2e

feat(data/padic/padic_integers): homs to zmod(p ^ n) (#3882)

jcommelin committed 5 years ago

44787193

chore(set_theory/game): various cleanup and code golf (#3939)

TwoFX committed 5 years ago

b03ce616

Newer Older