leanprover-community/mathlib3

Pull Requests Commits

LAC1213 committed 4 years ago

1875f69e

A local noetherian integral domain of Krull dim 1 with principal maximal ideal is a DVR

LAC1213 committed 4 years ago

d88eb641

laughinggas committed 5 years ago

cde5f15f

Merge branch 'bernoulli-polynomials' of https://github.com/leanprover-community/mathlib into dd-iff

laughinggas committed 5 years ago

fcfc13f8

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

leanprover-community-bot committed 5 years ago

b846aa52

refactor(combinatorics/simple_graph): move simple graph files to their own folder (#5154)

agusakov committed 5 years ago

c3f4d1b8

feat(linear_algebra/determinant): Show that the determinant is a multilinear map (#5142)

eric-wieser committed 5 years ago

e3a699ed

feat(ring_theory/integral_closure): Cleanup interface for ring_hom.is_integral (#5144)

dtumad committed 5 years ago

9f955fe5

feat(category_theory/limits): reflexive coequalizers (#5123)

b-mehta committed 5 years ago

1f1ba587

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

leanprover-community-bot committed 5 years ago

5866812c

feat(tactic/explode): display exploded proofs as widgets (#4718)

minchaowu committed 5 years ago

fe7b407f

chore(group_theory/perm/sign): Add swap_mul_involutive (#5141)

eric-wieser committed 5 years ago

ec822277

feat(category_theory/limits): images, equalizers and pullbacks imply functorial images (#5140)

TwoFX committed 5 years ago

916bf74a

chore(algebra/char_p): refactor char_p (#5132)

kckennylau committed 5 years ago

b1d8b897

feat(analysis/normed_space/dual): Fréchet-Riesz representation for the dual of a Hilbert space (#4379)

dupuisf committed 5 years ago

137163a8

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

leanprover-community-bot committed 5 years ago

801dea94

doc(field_theory/finite/basic): update doc-strings (#5134)

riccardobrasca committed 5 years ago

ba43f6f1

chore({ring,group}_theory/free_*): Add of_injective (#5131)

eric-wieser committed 5 years ago

b6f23099

feat(ring_theory/polynomials/cyclotomic): add lemmas about cyclotomic polynomials (#5122)

riccardobrasca committed 5 years ago

4a153ed9

feat(ring_theory/jacobson): generalized nullstellensatz - polynomials over a Jacobson ring are Jacobson (#4962)

dtumad committed 5 years ago

14f20960

chore(category_theory/limits): golf a proof (#5133)

TwoFX committed 5 years ago

8d3e93fb

feat(algebra/group/basic): simplify composed assoc ops (#5031)

pechersky committed 5 years ago

fb704197

feat(ring_theory/witt_vector/init_tail): adding disjoint witt vectors (#4835)

jcommelin committed 5 years ago

73a2fd3a

feat(topology/separation): Adds t2_space instances for disjoint unions (sums and sigma types). (#5113)

adamtopaz committed 5 years ago

396487f9

feat(field_theory/separable): add separable_of_X_pow_sub_C and squarefree_of_X_pow_sub_C (#5052)

riccardobrasca committed 5 years ago

876481ef

feat(category_theory/sites): the canonical topology on a category (#4928)

b-mehta committed 5 years ago

c82b7082

feat(data/fin): Add pred_{le,lt}_pred_iff (#5121)

eric-wieser committed 5 years ago

0ac414af

chore(topology/path_connected): move `proj_Icc` to a separate file (#5120)

urkud committed 5 years ago

8acd296e

chore(category_theory/limits): golf a proof (#5130)

TwoFX committed 5 years ago

238c58c3

feat(logic/relation): trans_gen closure (#5129)

pechersky committed 5 years ago

ff2aeae9

Older