leanprover-community/mathlib3

Pull Requests Commits

feat(ring_theory/local_properties): Being finite / of finite type is local. (#10775)

erdOne committed 4 years ago

56033982

feat(order): define a `rel_hom_class` for types of relation-preserving maps (#10755)

Vierkantor committed 4 years ago

c10a8728

feat(algebraic_geometry): A scheme is reduced iff its stalks are reduced. (#10879)

erdOne committed 4 years ago

af682d35

feat(analysis/calculus/deriv): add `has_deriv_at.tendsto_punctured_nhds` (#10877)

urkud committed 4 years ago

65118e5f

feat(ring_theory/integral_closure): A subalgebra is contained in the integral closure iff it is integral (#10874)

tb65536 committed 4 years ago

01088844

feat(algebra/algebra/subalgebra): Elements of supremum (#10872)

tb65536 committed 4 years ago

7de517b2

feat(algebra/algebra/subalgebra): Lemmas about `alg_hom.range` (#10871)

tb65536 committed 4 years ago

df113020

feat(algebraic_geometry): The underlying topological space of a Scheme is T0 (#10869)

erdOne committed 4 years ago

ac10136f

feat(data/int): various lemmas (#10862)

Ruben-VandeVelde committed 4 years ago

cb0a6f70

feat(algebra/group/basic): add a few lemmas (#10856)

urkud committed 4 years ago

04e2f5f7

feat(analysis/normed_space/lattice_ordered_group): prove `order_closed_topology` for `normed_lattice_add_comm_group` (#10838)

RemyDegenne committed 4 years ago

5859ec0f

removed useless instance

jjaassoonn committed 4 years ago

93ccd061

jjaassoonn committed 4 years ago

91f14f21

chore(*): more assorted proof simplifications (#10863)

alexjbest committed 4 years ago

6353d6b2

refactor(*): kill a few uses of finish (#10860)

sgouezel committed 4 years ago

0e995a37

feat(field_theory/intermediate_field): Range of `intermediate_field.val` (#10873)

tb65536 committed 4 years ago

ec2f3509

feat(category_theory): Glue data (#10436)

erdOne committed 4 years ago

718ea932

chore(algebra/algebra/basic): fix instances names to make doc links work (#10834)

eric-wieser committed 4 years ago

a252427a

less profunctory doc

jjaassoonn committed 4 years ago

3ccb8163

jjaassoonn committed 4 years ago

234259b4

delte unnecessary thiings

jjaassoonn committed 4 years ago

7709e89c

jjaassoonn committed 4 years ago

c793b338

feat(data/finset/basic): add to_list_insert and to_list_cons (#10840)

Jlh18 committed 4 years ago

2043748c

finished descent

jjaassoonn committed 4 years ago

5203f7ae

jjaassoonn committed 4 years ago

00a92341

feat(measure_theory/integral/bochner): prove `set_integral_eq_subtype` (#10858)

urkud committed 4 years ago

fc09b17f

feat(data/nat): decidable exists le instance (#10857)

b-mehta committed 4 years ago

86493f12

feat(algebra/group/hom): generalize `semiconj_by.map` and `commute.map` (#10854)

Vierkantor committed 4 years ago

70f4ba07

feat(data/finset/basic): add ite_subset_union, inter_subset_ite for finset (#10586)

alexjbest committed 4 years ago

0b5f0a2d

feat(data/finsupp/basic): add two versions of `finsupp.mul_prod_erase` (#10708)

stuart-presnell committed 4 years ago

e5a844e1

Newer Older