leanprover-community/mathlib

Pull Requests Commits

Specialize surj_units to decidable_pred over whole type

pechersky committed 2 years ago

4ff1df1a

refactor infinite prod to be over units topology

pechersky committed 2 years ago

d994929a

continuous_on surj_units

pechersky committed 2 years ago

ebc76f7c

Another specific example

pechersky committed 2 years ago

32b54b64

pechersky committed 2 years ago

a4db4be0

pechersky committed 2 years ago

26a32394

rearrange files

pechersky committed 2 years ago

d1a0025a

Merge branch 'master' into 2301.10303

pechersky committed 2 years ago

6cfdab13

docs(algebra/module/equiv): correct a misleading comment (#18458)

eric-wieser committed 2 years ago

ea94d7cd

converges_prod_one_sub_iff_summable

pechersky committed 2 years ago

9922fd43

refactor(topology/metric_space): drop `dist_setoid` (#18502)

urkud committed 2 years ago

0c1f285a

feat(matrix/dual_number): `matrix` and `dual_number` commute (#18386)

eric-wieser committed 2 years ago

eb0cb451

chore(number_theory/pell*): rename files, update doc (#18503)

MichaelStollBayreuth committed 2 years ago

a66d07e2

feat(set_theory/ordinal/fixed_point): add missing theorem (#18323)

vihdzp committed 2 years ago

c6b53304

fix (measure_theory/measure/measure_space_def): fix module docstring typos (#18500)

kbuzzard committed 2 years ago

146a2eed

docs(set_theory/lists): update docs (#18346)

astrainfinita committed 2 years ago

497d1e06

chore(data/finset/lattice): Protect a few more lemmas (#18497)

YaelDillies committed 2 years ago

1c857a1f

feat(data/polynomial/div): prove that evaluation induces an isomorphism of algebras (#18480)

Multramate committed 2 years ago

e064a7bf

feat(number_theory/pell_general): add general existence result for Pell's Equation (#18484)

MichaelStollBayreuth committed 2 years ago

c23aca35

feat(analysis/fourier): Poisson summation (#18392)

loefflerd committed 2 years ago

3353f337

feat(probability/probability_mass_function): construct a `pmf` from a probability measure (#18270)

dtumad committed 2 years ago

3f5c9d30

chore(measure theory/group/measure): Generalize typeclasses (#18496)

YaelDillies committed 2 years ago

950605e4

feat(number_theory/number_field/embeddings): some additional lemmas (#18473)

xroblot committed 2 years ago

271bf175

feat(measure_theory/integral): integration lemmas from #18392 (#18466)

loefflerd committed 2 years ago

733fa004

feat(analysis/convex/body): endow with Hausdorff metric (#16338)

datokrat committed 2 years ago

858a10cf

chore(data/set/basic): Golf #18356 (#18491)

YaelDillies committed 2 years ago

75608aff

feat(*/with_top): add lemmas about `with_top`/`with_bot` (#18487)

urkud committed 2 years ago

afdb4fa3

feat(geometry/manifold/vector_bundle): `smooth_fiberwise_linear` groupoid (#17302)

hrmacbeth committed 2 years ago

5be98b95

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring (#14249)

mariainesdff committed 2 years ago

a8e7ac80

chore(data/real/nnreal): drop some lemmas (#18492)

urkud committed 2 years ago

b2ff9a3d

Older