Commits leanprover-community/mathlib

feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations (#16860)

Multramate committed 3 years ago

5f17f4da

feat(group_theory/subgroup/basic): Multiplication of disjoint subgroups is injective (#16966)

tb65536 committed 3 years ago

158724c8

feat(order/upper_lower): Product of upper sets (#17022)

mans0954 committed 3 years ago

0c171f29

feat(ring_theory/finiteness): Kernel of surjective morphism between finitely presented algebras is fg. (#15969)

erdOne committed 3 years ago

2f5533c9

feat(order/locally_finite): add lemmas expanding `finset.Icc` (#16996)

eric-wieser committed 3 years ago

e905eeab

feat(algebra/order/floor): several round and fract lemmas (#17001)

alexjbest committed 3 years ago

64505769

feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category (#14402)

manzyuk committed 3 years ago

4698e35c

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

leanprover-community-bot committed 3 years ago

6568f2f2

feat(group_theory/subgroup/basic): Range and kernel of `monoid_hom.restrict` (#16988)

tb65536 committed 3 years ago

71a759b2

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