leanprover-community/mathlib3

Pull Requests Commits

chore(*): a few more lemmas with removable edge cases

alexjbest committed 4 years ago

f3726e8d

chore(topology/continuous_function/bounded): remove extra typeclass assumption (#10823)

hrmacbeth committed 4 years ago

ef69cac1

feat(algebra/module/linear_map): interaction of linear maps and pointwise operations on sets (#10821)

sgouezel committed 4 years ago

00c55f5e

feat(analysis/special_functions/complex): range of `complex.exp (↑x * I)` (#10816)

urkud committed 4 years ago

dfb78f7e

feat(analysis/mean_inequalities): corollary of Hölder inequality (#10789)

hrmacbeth committed 4 years ago

81e58c9e

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

Older