leanprover-community/mathlib

Pull Requests Commits

bottine committed 2 years ago

47d86b61

Distinct universes for isomorphic quivers.

bottine committed 2 years ago

30301772

Distinct universes for iso

bottine committed 2 years ago

a905ef45

bottine committed 2 years ago

6831b3f9

Update src/combinatorics/quiver/iso.lean

bottine committed 2 years ago

Verified b57e2e8c

bottine committed 2 years ago

Verified 3b702a7d

to launch the CI again

bottine committed 2 years ago

af46d30e

Yael's review, easy parts

bottine committed 2 years ago

b9ac8bd0

bottine committed 2 years ago

8f2d3797

chore(algebra/module/linear_map): move `map_sum` lemmas (#18106)

hrmacbeth committed 2 years ago

40acfb6a

feat(analysis/fourier): convergence of Fourier series (#17913)

loefflerd committed 2 years ago

247a102b

feat(measure_theory/integral): "integral_prod_mul" for complex coefficients (#18085)

loefflerd committed 2 years ago

7c60702a

feat(data/{set,finset}/basic): Convenience lemmas (#17957)

YaelDillies committed 2 years ago

bc7d81be

feat(field_theory/chevalley_warning): Binary version (#18083)

YaelDillies committed 2 years ago

e001509c

chore(algebra/group_ring_action/invariant): streamline imports (#18092)

hrmacbeth committed 2 years ago

e7bab9a8

chore(number_theory/pell): golf, use tactic mode (#18091)

urkud committed 2 years ago

5a1fa97e

feat(topology/instances/add_circle): generalize `homeo_Icc_quot` from ℝ to archimedean groups (#17983)

alreadydone committed 3 years ago

940d3713

feat(ring_theory/ideal/basic): allow noncommutativity in `span_singleton_mul_left_unit` (#18088)

alreadydone committed 3 years ago

ae0f31c7

feat(analysis/convolution): regularity of convolution for functions depending on a parameter (#17626)

sgouezel committed 3 years ago

9d81ef7e

feat(probability/kernel/basic): measurability of the integral against a kernel (#18061)

RemyDegenne committed 3 years ago

2bb0d084

feat(data/real/ennreal): `mul_div_mul_left` (#18051)

madvorak committed 3 years ago

ad1c83e8

feat(combinatorics/simple_graph/connectivity): `walk.to_subgraph` (#17325)

kmill committed 3 years ago

d6e84a0d

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

leanprover-community-bot committed 3 years ago

10708587

chore(algebra/continued_fractions): golf some proofs (#18082)

urkud committed 3 years ago

134625f5

feat(analysis/convex): add lemma for composition of convex functions (#15111)

ericluap committed 3 years ago

14e84382

chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy (#18065)

Paul-Lez committed 3 years ago

3e00d81b

feat(data/set/finite): Align `set.to_finset` and `set.finite.to_finset` (#17959)

YaelDillies committed 3 years ago

117e93f8

feat(data/set/function): `∘` lemmas (#17819)

YaelDillies committed 3 years ago

67f36267

feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts (#17668)

fpvandoorn committed 3 years ago

e6444585

chore(analysis/normed_space/lp_equiv): fix docs (#18073)

ericrbg committed 3 years ago

6afc9b06

Older