leanprover-community/mathlib3

Pull Requests Commits

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

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

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

Jlh18 committed 4 years ago

2043748c

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

feat(algebra/algebra): instantiate `ring_hom_class` for `alg_hom` (#10853)

Vierkantor committed 4 years ago

c9fe6d1a

feat(ring_theory/noetherian): fg_pi (#10845)

eric-wieser committed 4 years ago

ba24b38b

feat(data/set/function): Cancelling composition on a set (#10803)

YaelDillies committed 4 years ago

5a598003

feat(combinatorics/configuration): New file (#10773)

tb65536 committed 4 years ago

6838233f

feat(data/nat/count): The count function on naturals (#9457)

kim-em committed 4 years ago

8743573e

chore(algebra/associated): split off dependencies of `big_operators` (#10848)

Vierkantor committed 4 years ago

081cb8ab

feat(algebra/big_operators/basic): add finset.prod_to_list (#10842)

Jlh18 committed 4 years ago

862a68c9

feat(topology/subset_properties): open/closed sets are locally compact spaces (#10844)

urkud committed 4 years ago

5558fd9f

feat(combinatorics/simple_graph/basic): Incidence set lemmas (#10839)

YaelDillies committed 4 years ago

b100af69

refactor(category_theory/sites/*): Redefine the category of sheaves. (#10678)

adamtopaz committed 4 years ago

9f9015c6

fix(ring_theory/ideal/basic): remove universe restriction (#10843)

eric-wieser committed 4 years ago

601f2ab7

chore(field_theory/ratfunc): to_fraction_ring_ring_equiv (#10806)

eric-wieser committed 4 years ago

905d887f

chore(field_theory/ratfunc): has_scalar in terms of localization (#10828)

pechersky committed 4 years ago

eeef771d

feat(data/set/function): Congruence lemmas for `monotone_on` and friends (#10817)

YaelDillies committed 4 years ago

542471fd

feat(ring_theory/local_property): Being reduced is a local property. (#10734)

erdOne committed 4 years ago

b5b19a69

Newer Older