leanprover-community/mathlib

Pull Requests Commits

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

chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836)

hrmacbeth committed 4 years ago

68ced9a9

feat(measure_theory/measure): new class is_finite_measure_on_compacts (#10827)

sgouezel committed 4 years ago

d212f3eb

feat(category_theory/adjunction/evaluation): Evaluation has a left and a right adjoint. (#10793)

adamtopaz committed 4 years ago

87e2f24b

chore(data/polynomial/field_division): beta-reduce (#10835)

gebner committed 4 years ago

8e4b3b0f

chore(*): tweaks taken from gh-8889 (#10829)

eric-wieser committed 4 years ago

5a835b7b

feat(analysis/normed_space/basic): formula for `c • sphere x r` (#10814)

urkud committed 4 years ago

8218a788

Newer Older