leanprover-community/mathlib3

Pull Requests Commits

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

feat(topology/metric_space/isometry): (pre)image of a (closed) ball or a sphere (#10813)

urkud committed 4 years ago

b82c0d25

feat(topology/metric_space/hausdorff_distance): add more topological properties API to thickenings (#10661)

kkytola committed 4 years ago

21c9d3b3

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

Newer Older