leanprover-community/mathlib3

Pull Requests Commits

revert finset changes

eric-wieser committed 3 years ago

91a0aa30

fix decidable arguments

eric-wieser committed 3 years ago

82eb6699

eric-wieser committed 3 years ago

3c3c67b6

eric-wieser committed 3 years ago

341f8e61

chore(data/finset/locally_finite): add more lemmas about one-sided intervals

eric-wieser committed 3 years ago

3e88bb32

feat(data/polynomial): a couple of lemmas on nat degree and roots of maps (#16992)

alexjbest committed 3 years ago

d8dd620c

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is. (#15949)

erdOne committed 3 years ago

cf94743b

feat(topology/subset_properties, noetherian_space): Noetherian spaces have finite irreducible components. (#17015)

erdOne committed 3 years ago

6d94ff7b

refactor(geometry/manifold/cont_mdiff): split everything about mfderiv (#16982)

fpvandoorn committed 3 years ago

2b69cd5e

style(geometry/euclidean): consistently use inner product notation (#16961)

jsm28 committed 3 years ago

3c95a727

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

Older