leanprover-community/mathlib3

Pull Requests Commits

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

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

refactor(analysis/normed_space/hahn_banach): use is_R_or_C instead of specific typeclass (#5009)

sgouezel committed 5 years ago

17a6f6da

chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (#5066)

kbuzzard committed 5 years ago

2a876b65

chore(data/fin): a few more lemmas about `fin.insert_nth` (#5079)

urkud committed 5 years ago

8d71ec99

chore(topology/metric_space/isometry): add a missing simp lemma (#5078)

urkud committed 5 years ago

c4587245

chore(algebra/big_operators): add `finset.abs_prod` (#5076)

urkud committed 5 years ago

a9b6b362

chore(measure_theory/borel_space): add some `simp` attrs (#5075)

urkud committed 5 years ago

2ba930eb

chore(topology/basic): add `cluster_pt.map`, rename `mem_closure` (#5065)

urkud committed 5 years ago

c59dbf3d

chore(analysis/complex/basic): add `times_cont_diff.real_of_complex` (#5073)

urkud committed 5 years ago

a6498516

chore(logic/basic): add `forall_apply_eq_imp_iff₂` (#5072)

urkud committed 5 years ago

87439b98

Newer Older