leanprover-community/mathlib

Pull Requests Commits

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

feat(data/polynomial/eval): eval₂ f x (p * X) = eval₂ f x p * x (#5110)

urkud committed 5 years ago

af7ba87a

chore(order/basic): add `strict_mono_??cr_on.dual` and `dual_right` (#5107)

urkud committed 5 years ago

8e09111f

chore(category_theory/iso): golf and name consistency (#5096)

b-mehta committed 5 years ago

a106102a

feat(linear_algebra/bilinear_form): equivalence with matrices, given a basis (#5095)

Vierkantor committed 5 years ago

d0789503

feat(number_theory/arithmetic_function): Moebius inversion (#5047)

awainverse committed 5 years ago

c06c6169

feat(field_theory): Prove the Galois correspondence (#4786)

tb65536 committed 5 years ago

2bda184a

chore(data/equiv/basic): redefine `set.bij_on.equiv` (#5128)

urkud committed 5 years ago

2f939e93

chore(data/set/function): add 3 trivial lemmas (#5127)

urkud committed 5 years ago

4715d992

chore(data/complex/exponential): golf 2 proofs (#5126)

urkud committed 5 years ago

c1edbdda

doc(data/equiv/basic): improve docstring of `equiv.sum_equiv_sigma_bool` (#5119)

urkud committed 5 years ago

cb9e5cf9

chore(data/pprod): Add pprod.mk.eta (#5114)

eric-wieser committed 5 years ago

d3cc9935

chore(order/rel_iso): add a few lemmas (#5106)

urkud committed 5 years ago

2c5d4a3c

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

leanprover-community-bot committed 5 years ago

1a8089e9

chore(data/sum): Add trivial simp lemmas (#5112)

eric-wieser committed 5 years ago

59717d68

chore(data/equiv/basic): Add comp_swap_eq_update (#5091)

eric-wieser committed 5 years ago

2d476e0e

Newer Older