leanprover-community/mathlib

Pull Requests Commits

chore(combinatorics/simple_graph): fix name mixup (#10785)

b-mehta committed 4 years ago

026e6929

feat(data/int/basic): more int.sign API (#10781)

pechersky committed 4 years ago

204aa7e8

chore(*): remove edge case assumptions from lemmas (#10774)

alexjbest committed 4 years ago

75b4e5f5

feat(data/{multiset, finset}/basic): add card_mono (#10771)

BoltonBailey committed 4 years ago

3f55e027

split(logic/nonempty): Split off `logic.basic` (#10762)

YaelDillies committed 4 years ago

a0b6bab2

refactor(order/sup_indep): Get rid of decidable equality assumption (#10673)

YaelDillies committed 4 years ago

02cdc812

feat(order/zorn): Added some results about chains (#10658)

vihdzp committed 4 years ago

9525f5e0

feat(measure_theory/integral/divergence_theorem): specialize for `f : ℝ → E` and `f g : ℝ × ℝ → E` (#10616)

urkud committed 4 years ago

accdb8fc

feat(data/set/lattice): new lemma Union_singleton_eq_range (#10819)

sgouezel committed 4 years ago

4ff9b82a

feat(logic/basic): When an If-Then-Else is not one of its arguments (#10800)

YaelDillies committed 4 years ago

dc732a3c

chore(*): introduce notation for left/right/punctured nhds (#10694)

urkud committed 4 years ago

7130d75d

refactor(order/basic): Change definition of `<` on `α × β` (#10667)

YaelDillies committed 4 years ago

6043522e

doc(algebra/algebra/basic): expand the docstring (#10221)

eric-wieser committed 4 years ago

6530769a

chore(computability/regular_expressions): eliminate `finish` (#10811)

stuart-presnell committed 4 years ago

bb51df36

feat(ring_theory/localization,group_theory/monoid_localization): other scalar action instances (#10804)

eric-wieser committed 4 years ago

5658241a

chore(analysis/special_functions/pow): remove duplicate lemmas concerning monotonicity of `rpow` (#10794)

j-loreaux committed 4 years ago

930ae468

doc(linear_algebra/std_basis): update module doc (#10818)

Vierkantor committed 4 years ago

61949afe

doc(undergrad): Link the affine group (#10797)

eric-wieser committed 4 years ago

9f787c2c

feat(data/finsupp/basic): Add `finsupp.erase_of_not_mem_support` (#10689)

stuart-presnell committed 4 years ago

c574e387

chore(data/sym/sym2): Better lemma names (#10801)

YaelDillies committed 4 years ago

03a250a4

chore(algebra/algebra/basic): alg_equiv.map_smul (#10805)

pechersky committed 4 years ago

40cfdecd

docs(undergrad): more links (#10790)

PatrickMassot committed 4 years ago

8f5031ae

feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction (#10713)

RemyDegenne committed 4 years ago

e3eb0eb0

feat(algebraic_geometry): LocallyRingedSpace has coproducts. (#10665)

erdOne committed 4 years ago

1367c19b

feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749)

Vierkantor committed 4 years ago

9078914e

chore(data/equiv/ring): inv_fun_eq_symm (#10779)

pechersky committed 4 years ago

f46a7a0f

feat(combinatorics/simple_graph): simp lemmas about spanning coe (#10778)

b-mehta committed 4 years ago

6d15ea43

feat(group_theory/order_of_element): additivize (#10766)

ericrbg committed 4 years ago

05d87671

chore(measure_theory/decomposition/signed_hahn): Fixed a few typos (#10777)

vihdzp committed 4 years ago

85cb4a81

move(algebra/order/lattice_group): Move from `algebra.lattice_ordered_group` (#10763)

YaelDillies committed 4 years ago

f070a69b

Newer Older