leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/lie/skew_adjoint): move logic for Lie algebras of skew-adjoint endomorphisms to own file (#5098)

Oliver Nash committed 5 years ago

fe4abe00

chore(group_theory/perm/sign): Golf a proof

eric-wieser committed 5 years ago

765613d9

Merge branch 'master' of github.com:leanprover-community/mathlib into algebra_multilinear_maps

eric-wieser committed 5 years ago

6aa9f5f0

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

leanprover-community-bot committed 5 years ago

51e71e9d

feat(data/finset/basic): Finset subset induction (#5087)

tb65536 committed 5 years ago

64b3e52b

feat(group_theory/perm/sign): Add swap_induction_on' (#5092)

eric-wieser committed 5 years ago

434a34de

feat(algebra/lie/direct_sum): direct sums of Lie modules (#5063)

Oliver Nash committed 5 years ago

2a49f4e5

feat(ring_theory/*): Various lemmas about ideals, quotients, and localizations (#5046)

dtumad committed 5 years ago

fee93e96

chore(linear_algebra/bilinear_form): cleanup (#5049)

Vierkantor committed 5 years ago

96a20388

fix(ring_theory/discrete_valuation_ring): docstring typos (#5085)

kbuzzard committed 5 years ago

270fc310

chore(category_theory/limits): move product isomorphisms (#5057)

b-mehta committed 5 years ago

e8c8ce91

feat(category_theory/limits): explicit binary product functor in Type (#5043)

b-mehta committed 5 years ago

a71901f2

feat(field_theory/separable): a separable polynomial is squarefree (#5039)

riccardobrasca committed 5 years ago

562be707

feat(category_theory/sigma): disjoint union of categories (#5020)

b-mehta committed 5 years ago

3c1cf603

feat(combinatorics/colex): introduce colexicographical order (#4858)

b-mehta committed 5 years ago

13b9478e

feat(analysis/normed_space/inner_product): inner product is infinitely smooth (#5089)

urkud committed 5 years ago

83ec6e06

chore(*): Fix linter error

eric-wieser committed 5 years ago

97bac667

chore(*): Fix proof broken by updates to fin in core lean

eric-wieser committed 5 years ago

8f7b07e7

chore(*): Remove definitions which now exist elsewhere

eric-wieser committed 5 years ago

ba169870

Merge remote-tracking branch 'origin/master' into algebra_multilinear_maps

eric-wieser committed 5 years ago

0efa5f53

feat(data/padics/padic_norm): add a little more API (#5082)

kbuzzard committed 5 years ago

fdabe9c3

feat(analysis/special_functions/exp_log): `exp` is infinitely smooth (#5086)

urkud committed 5 years ago

2f516593

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

leanprover-community-bot committed 5 years ago

b9bd4a57

feat(data/nat/basic): add injectivity and divisibility lemmas (#5068)

kbuzzard committed 5 years ago

ce0498e6

chore(data/list/basic): Add pmap_map (#5081)

eric-wieser committed 5 years ago

2252c3a0

chore(order/basic): add `le_update_iff` and `update_le_iff` (#5080)

urkud committed 5 years ago

7f4286c9

chore(logic/unique): add `fin.inhabited` (#5077)

urkud committed 5 years ago

c4132e9a

chore(data/real/ennreal): add a few lemmas (#5071)

urkud committed 5 years ago

20444517

chore(data/set/basic): more simp lemmas (#5070)

urkud committed 5 years ago

f627d765

feat(finset/basic): Add forall_mem_union (#5064)

b-mehta committed 5 years ago

f5b967ac

Newer Older