leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 3 years ago

78a48297

docs(*): Missing undergrad and overview items (#17003)

PatrickMassot committed 3 years ago

4d8fe495

feat(data/set/function): add `set.eq_on_union` (#16984)

urkud committed 3 years ago

5ea225ec

feat(algebra/group_ring_action): add `mul_semiring_action.comp_hom` (#16850)

mkaratarakis committed 3 years ago

0fecc32c

fix(*): use `old_structure_cmd` for all morphism classes (#16242)

dupuisf committed 3 years ago

11c53f17

feat(algebra/ring): mark a useful lemma simp and generalize unit neg lemmas (#16993)

alexjbest committed 3 years ago

86bf83ab

chore(analysis/normed_space/operator_norm): fix naming of `continuous_linear_map.lmul` and similar (#15968)

j-loreaux committed 3 years ago

583cae77

feat(data/polynomial): a lemma relating `nth_roots 2` to `is_square` (#16990)

alexjbest committed 3 years ago

3605313c

feat(topology/algebra/module/basic): a hyperplane is either closed or dense (#16782)

ADedecker committed 3 years ago

e05f1302

feat(logic/lemmas): Aliases for `=`-`≠` transitivity lemmas (#16959)

YaelDillies committed 3 years ago

4a4d740d

feat(algebra/star/subalgebra): develop some API for `star_subalgebra` (#16896)

j-loreaux committed 3 years ago

0a375900

feat(algebra/ring/aut): add apply_mul_semiring_action & mul_semiring_action.to_ring_aut (#16857)

mkaratarakis committed 3 years ago

73c9121e

feat(topology/metric_space/infsep): Add "infimum separation". (#15689)

linesthatinterlace committed 3 years ago

5316314b

chore(algebra/group/*): attribute copyright properly, correct instance names (#16967)

YaelDillies committed 3 years ago

372310d0

feat(analysis/inner_product_space/two_dim): volume/area form of negated orientation (#16939)

hrmacbeth committed 3 years ago

5d7ab6e9

refactor(data/finset/noncomm_prod): Use `set.pairwise` (#16859)

YaelDillies committed 3 years ago

31263840

feat(data/multiset/basic): multiset inclusion is decidable (#16994)

eric-wieser committed 3 years ago

7121691d

feat(analysis/complex/open_mapping): the open mapping thm for holomorphic functions (#16780)

vbeffara committed 3 years ago

5c19b83b

feat(probability/independence): Kolmogorov's 0-1 law (#16648)

RemyDegenne committed 3 years ago

da4010c2

feat(topology/algebra/order/basic): `nhds_within` versions (#16956)

YaelDillies committed 3 years ago

e6f28f56

feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le` (#16951)

kex-y committed 3 years ago

f6b12763

fix(topology/metric_space/lipschitz): typo (#16962)

fpvandoorn committed 3 years ago

e623a7e4

refactor(combinatorics/young_tableau): move young diagram modules (#16954)

jakelev committed 3 years ago

34f53b6c

feat(topology/metric_space/emetric_space): `nhds_within` lemmas (#16952)

YaelDillies committed 3 years ago

4c2452e8

feat(analysis/normed_space/star/gelfand_duality): functoriality of `character_space ℂ` (#16835)

j-loreaux committed 3 years ago

e0ce2186

feat(analysis/bounded_variation): functions of bounded variation are ae differentiable (#16680)

sgouezel committed 3 years ago

71429ce7

feat(category_theory/groupoid/subgroupoid): subgroupoids and basic properties (#16742)

alreadydone committed 3 years ago

7a52b9ce

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

leanprover-community-bot committed 3 years ago

8f9520eb

refactor(geometry/euclidean/basic): rename `cospherical_subset` (#16947)

jsm28 committed 3 years ago

1e9b3df5

feat(analysis/inner_product_space/two_dim): new file (#16928)

hrmacbeth committed 3 years ago

a08db7e9

Older