leanprover-community/mathlib3

Pull Requests Commits
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
Remove lock
ADedecker committed 4 years ago
06f772b3
Merge branch 'bounded_of_bdd_above_of_bdd_below' into monotone_integrable
ADedecker committed 4 years ago
0881effa
Content
ADedecker committed 4 years ago
485c88af
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
Factor variables
ADedecker committed 4 years ago
c6e0971f
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
Terms Of Use Privacy Policy Refund Policy Impressum