leanprover-community/mathlib3

Pull Requests Commits

hrmacbeth committed 4 years ago

7de147c0

hrmacbeth committed 4 years ago

f1c5d006

Merge remote-tracking branch 'origin/master' into affine-equiv-lemmas

hrmacbeth committed 4 years ago

6c2382f7

feat(order/filter/basic): add `supr_inf_principal` and `tendsto_supr` (#9051)

urkud committed 4 years ago

d0c02bc9

chore(analysis/normed_space): add `dist_sum_sum_le` (#9049)

urkud committed 4 years ago

6b0c73a0

chore(data/bool): add a few lemmas about inequalities and `band`/`bor` (#9048)

urkud committed 4 years ago

3fdfc8e5

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

leanprover-community-bot committed 4 years ago

c4f37076

docs(set_theory/lists): add module docstring and def docstrings (#8967)

YaelDillies committed 4 years ago

77f4ed46

feat(topology/uniform_space/basic): add corollary of Lebesgue number lemma `lebesgue_number_of_compact_open` (#8963)

ocfnash committed 4 years ago

0c19d5f5

feat(data/matrix/hadamard): add the Hadamard product (#8956)

l534zhan committed 4 years ago

a7be93b2

feat(group_theory/subgroup): Normal Core (#8940)

tb65536 committed 4 years ago

91824e58

feat(*): trivial lemmas from #8903 (#8909)

urkud committed 4 years ago

298f231e

chore(linear_algebra/tensor_product): remove `@[ext]` tag from `tensor_product.mk_compr₂_inj` (#8868)

dupuisf committed 4 years ago

5b29630d

feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine independence (#8892)

ocfnash committed 4 years ago

ceb9da60

feat(group_theory/perm/concrete_cycle): is_cycle_form_perm (#8859)

pechersky committed 4 years ago

5eb19182

feat(linear_algebra): introduce notation for `linear_map.comp` and `linear_equiv.trans` (#8857)

dupuisf committed 4 years ago

f157b6df

feat(group_theory/nilpotent): add antimono and functorial lemma for lower central series (#8853)

ineswright committed 4 years ago

d2625006

feat(tactic/lint): reducible non-instance linter (#8540)

fpvandoorn committed 4 years ago

f0f6c1cc

feat(algebra/ordered_monoid): correct definition (#8877)

kim-em committed 4 years ago

d6a1fc02

feat(order/prime_ideal): prime ideals are maximal (#9004)

atarnoam committed 4 years ago

ce31c1c6

refactor(topology/sheaves/sheaf_condition): Generalize unique gluing API (#9002)

justus-springer committed 4 years ago

54315218

feat(linear_algebra/affine_space/affine_equiv): affine homotheties as equivalences (#8983)

ocfnash committed 4 years ago

d472c56c

feat(linear_algebra/basis): a nontrivial module has nonempty bases (#9040)

Vierkantor committed 4 years ago

309674d9

feat(linear_algebra/smodeq): sub_mem, eval (#8993)

jcommelin committed 4 years ago

3218c373

feat(*): make more non-instances reducible (#8941)

fpvandoorn committed 4 years ago

fde1fc28

feat(data/multiset/basic): Add a result on intersection of multiset with `repeat a n` (#9038)

Paul-Lez committed 4 years ago

bfcf73fa

feat(field_theory/algebraic_closure): polynomials in an algebraically closed fields have roots (#9037)

ChrisHughes24 committed 4 years ago

3148cfe1

chore(data/nat/mul_ind): make docgen happy (#9036)

ericrbg committed 4 years ago

3a624194

feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors (#9034)

Vierkantor committed 4 years ago

11284f2f

feat(set/lattice): two lemmas about when sInter is empty (#9033)

atarnoam committed 4 years ago

86dd706c

Older