leanprover-community/mathlib

Pull Requests Commits

one erroneous translation

Antoine Chambert-Loir committed 2 years ago

416944d0

Antoine Chambert-Loir committed 2 years ago

5b87850b

feat(topology/algebra/infinite_sum) : infinite products

Antoine Chambert-Loir committed 2 years ago

181e1172

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

apurvnakade committed 2 years ago

147b2943

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

leanprover-community-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)

leanprover-community-bot committed 2 years ago

30faa0c3

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

leanprover-community-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)

leanprover-community-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)

leanprover-community-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

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

leanprover-community-bot committed 2 years ago

e8e130de

refactor(data/matrix/invertible): more results about invertible matrices (#19204)

eric-wieser committed 2 years ago

722b3b15

feat(geometry/manifold/sheaf/basic): sheaf of functions satisfying a `local_invariant_prop` (#19146)

hrmacbeth committed 2 years ago

431589bc

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

leanprover-community-bot committed 2 years ago

f2ad3645

refactor(geometry/manifold/cont_mdiff_map): redefine as subtype not structure (#19147)

hrmacbeth committed 2 years ago

86c29aef

chore(data/zmod/algebra): make zmod.algebra a def (#19197)

riccardobrasca committed 2 years ago

0723536a

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

leanprover-community-bot committed 2 years ago

e160cefe

Older