leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' of https://github.com/leanprover-community/mathlib into group-coh-newer

101damnations committed 2 years ago

815458f8

chore(topology/sheaves): revert universe generalizations from #19153 (#19230)

kim-em committed 2 years ago

5dc6092d

chore(*): add mathlib4 synchronization comments (#19226)

github-actions[bot] committed 2 years ago

728ef9db

refactor: redefine `bundle.total_space` (#19221)

urkud committed 2 years ago

e473c319

feat(linear_algebra/matrix/schur_complement): invertibility of block matrices (#19156)

eric-wieser committed 2 years ago

a176cb12

chore(scripts): update nolints.txt (#19227)

leanprover-community-bot committed 2 years ago

44b3f423

chore(*): add mathlib4 synchronization comments (#19220)

github-actions[bot] committed 2 years ago

d0b19368

refactor(*): move all `mk_simp_attribute` commands to 1 file (#19223)

urkud committed 2 years ago

48fb5b52

chore(category_theory/concrete_category): reorder universes (#19222)

kim-em committed 2 years ago

311ef8c4

chore(*): add mathlib4 synchronization comments (#19218)

github-actions[bot] committed 2 years ago

9240e8be

feat(analysis/convex/cone/proper): add hyperplane_separation and comap (#19008)

apurvnakade committed 2 years ago

147b2943

chore(*): add mathlib4 synchronization comments (#19216)

github-actions[bot] committed 2 years ago

08b63ab5

chore(category_theory/limits/construction/over): rename default to basic (#19217)

kim-em committed 2 years ago

15db1b4f

feat(analysis/inner_product_space): the adjoint for unbounded operators (#18820)

mcdoll committed 2 years ago

8b981918

feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card (#19198)

AntoineChambert-Loir committed 2 years ago

3ff3f2d6

chore(*): add mathlib4 synchronization comments (#19215)

github-actions[bot] committed 2 years ago

30faa0c3

chore(*): add mathlib4 synchronization comments (#19214)

github-actions[bot] committed 2 years ago

fdc286cc

feat(topology/metric_space/dilation): Dilations on metric spaces (#14315)

winston-h-zhang committed 2 years ago

93f88091

chore(*): add mathlib4 synchronization comments (#19213)

github-actions[bot] committed 2 years ago

5d0c7689

chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds (#19212)

urkud committed 2 years ago

57f9349f

feat(group_theory): simple lemmas for Wedderburn (#18862)

ericrbg committed 2 years ago

d30d3126

chore(*): add mathlib4 synchronization comments (#19211)

github-actions[bot] committed 2 years ago

1b089e3b

feat(analysis/normed_space/multilinear): add lemmas/defs (#19114)

urkud committed 2 years ago

f4047663

feat(order/monotone): add `decidable` instances (#19175)

ericrbg committed 2 years ago

554bb38d

chore(topology/algebra/module/basic): generalize `to_span_singleton` to topological spaces (#19116)

eric-wieser committed 2 years ago

6285167a

feat(topology/algebra/order/compact): remove conditional completeness assumption in `is_compact.exists_forall_le` (#18991)

ADedecker committed 2 years ago

3efd324a

feat(data/finset/pointwise): `|s| ∣ |s * t|` (#18663)

YaelDillies committed 2 years ago

eba78710

feat(analysis/special_functions/log/base): add `real.logb_mul_base` (#18979)

slerpyyy committed 2 years ago

f23a09ce

feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions (#19209)

hrmacbeth committed 2 years ago

e5ab837f

feat(measure_theory/integral/average): Lebesgue average (#19199)

YaelDillies committed 2 years ago

c14c8fcd

Older