Commits leanprover-community/mathlib

feat(topology/basic): add two lemmas about frontier and two lemmas about preimages under continuous maps (#8329)

kkytola committed 4 years ago

048263d9

chore(order/boolean_algebra) : `compl_involutive` (#8357)

ericrbg committed 4 years ago

865e36bd

feat(measure_theory/hausdorff_measure): `dimH_{s,b,}Union`, `dimH_union` (#8351)

urkud committed 4 years ago

f45df472

feat(combinatorics/hales_jewett): Hales-Jewett and Van der Waerden (#8019)

dwarn committed 4 years ago

ad5afc21

feat(topology/subset_properties): add `countable_cover_nhds_within_of_sigma_compact` (#8350)

urkud committed 4 years ago

398027d5

chore(analysis/calculus/mean_value): use `nnnorm` in a few lemmas (#8348)

urkud committed 4 years ago

7d754e06

feat(topology/algebra/ordered): add `nhds_top_basis_Ici` and `nhds_bot_basis_Iic` (#8349)

urkud committed 4 years ago

3782c193

feat(measure_theory/hausdorff_measure): μH and dimH of a `subsingleton` (#8347)

urkud committed 4 years ago

8139d7eb

chore(data/real/ennreal): move `x ≠ 0` case of `mul_infi` to `mul_infi_of_ne` (#8345)

urkud committed 4 years ago

fcde3f0e

chore(analysis/normed_space/operator_norm): use `norm_one_class` (#8346)

urkud committed 4 years ago

bd56531b

chore(algebra/ring/basic): drop commutativity assumptions from some division lemmas (#8334)

Ruben-VandeVelde committed 4 years ago

93a37647

refactor(analysis/analytic/basic): refactor `change_origin` (#8282)

urkud committed 4 years ago

d4c0a118

feat(category_theory/subobject): subobject category equivalent to mono over category (#8304)

b-mehta committed 4 years ago

0cb634fb

feat(algebra/group_theory/lemmas): add int.pow_right_injective (#8278)

apurvnakade committed 4 years ago

e67e50f5

docs(measure_theory/integral_eq_improper): fix lemma names in docs (#8333)

ADedecker committed 4 years ago

10975e6d

feat(measure_theory/continuous_map_dense): continuous functions are dense in Lp (#8306)

hrmacbeth committed 4 years ago

8e3d9cee

chore(ring_theory/fractional_ideal): prefer `(⊤ : ideal R)` over `1` (#8298)

Vierkantor committed 4 years ago

a895300a

chore(linear_algebra/linear_independent): use `is_empty ι` instead of `¬nonempty ι` (#8331)

eric-wieser committed 4 years ago

42f7ca0f

feat(topology/metric_space/holder): define Hölder continuity (#8309)

urkud committed 4 years ago

9061ecc1

chore(topology/algebra/infinite_sum): relax the requirements on `has_sum.smul` (#8312)

eric-wieser committed 4 years ago

35a8d935

chore(set_theory/*): use `is_empty α` instead of `¬nonempty α` (#8276)

eric-wieser committed 4 years ago

162221fd

docs(order/rel_iso): add module docstring (#8249)

YaelDillies committed 4 years ago

9a801ef6

chore(algebra/quaternion): add `smul_mk` (#8126)

eric-wieser committed 4 years ago

e35d9760

feat(set_theory/cofinality): more infinite pigeonhole principles (#7879)

kim-em committed 4 years ago

610fab7a

feat(logic/embedding): simp lemma for injectivity for embeddings (#7881)

kim-em committed 4 years ago

e6ff367d

docs(data/fintype/basic): add module docstring (#8081)

YaelDillies committed 4 years ago

728eefec

chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325)

eric-wieser committed 4 years ago

4ae97924

feat(measure_theory/conditional_expectation): define condexp_L2, conditional expectation of L2 functions (#8324)

RemyDegenne committed 4 years ago

b577bb2c

feat(ring_theory/ideal): generalize two results from finset to multiset (#8320)

Vierkantor committed 4 years ago

79fbd465

feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303)

eric-wieser committed 4 years ago

a783a47c