leanprover-community/mathlib3

Pull Requests Commits

chore(logic/equiv/basic): split into two files (#17038)

kim-em committed 3 years ago

9407b033

fix(data/set/basic): Fix `set.lt_iff_ssubset`. (#17047)

erdOne committed 3 years ago

8c9b0057

feat(order/upper_lower): Maps of upper sets (#17007)

YaelDillies committed 3 years ago

4af7699b

fix(topology/metric_space/gromov_hausdorff): squeeze all simps (#17049)

fpvandoorn committed 3 years ago

3d197c69

feat(measure_theory/measure): `measure_Union_null_iff` for Props (#17029)

alexjbest committed 3 years ago

0b480ff9

chore(order/lattice): add lemmas about `sup` and `inf` on `prod` (#17040)

eric-wieser committed 3 years ago

3812c1ce

feat(scripts/port_status): script to show currently portable files (#17009)

kim-em committed 3 years ago

6d4f6107

feat(*): add various order-related lemmas (#16918)

ocfnash committed 3 years ago

a5347cb9

feat(analysis/calculus/cont_diff): strengthen lemma (#16933)

fpvandoorn committed 3 years ago

38992f94

feat(combinatorics/simple_graph/regularity/bound): `positivity` extension (#16639)

YaelDillies committed 3 years ago

8f774b71

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

Newer Older