leanprover-community/mathlib

Pull Requests Commits

Merge branch 'def_H_spaces' of https://github.com/alreadydone/mathlib into alreadydone-def_H_spaces

faenuccio committed 3 years ago

d9889c8b

remove unnecessary delayed_refl_right_e, golf

alreadydone committed 3 years ago

8466579c

left/right_Hmul_e: reverse order

alreadydone committed 3 years ago

a2b902f4

alreadydone committed 3 years ago

af1a2949

alreadydone committed 3 years ago

1998c371

golf with new Q_right

alreadydone committed 3 years ago

8ff63234

Update src/topology/homotopy/H_spaces.lean

faenuccio committed 3 years ago

Verified 063a9905

Update src/topology/homotopy/H_spaces.lean

faenuccio committed 3 years ago

Verified 8430b62d

Update src/topology/homotopy/H_spaces.lean

faenuccio committed 3 years ago

Verified 39ff9aae

Update src/topology/homotopy/H_spaces.lean

faenuccio committed 3 years ago

Verified 408e1d90

Update src/topology/homotopy/H_spaces.lean

faenuccio committed 3 years ago

Verified be866441

Update src/topology/homotopy/H_spaces.lean

faenuccio committed 3 years ago

Verified 4276ea2b

Merge branch 'master' into def_H_spaces

faenuccio committed 3 years ago

90cb8134

feat(measure_theory/integral/circle_integral_transform.lean): name ch… (#16387)

CBirkbeck committed 3 years ago

7df02f87

refactor(linear_algebra/affine_space/finite_dimensional): change three lemmas to instances (#16331)

jsm28 committed 3 years ago

06930844

feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#16290)

MichaelStollBayreuth committed 3 years ago

4b4975cf

feat(order/heyting/boundary): Co-Heyting boundary (#16257)

YaelDillies committed 3 years ago

0ab31714

feat(tactic/positivity): Handle division of integers (#16163)

YaelDillies committed 3 years ago

3a8665a8

feat(probability/martingale/basic): the stopped process of a submartingale is a submartingale (#16375)

RemyDegenne committed 3 years ago

44c90247

feat(linear_algebra/ray): `same_ray_map_iff` for injective linear maps (#16377)

jsm28 committed 3 years ago

dc8113b0

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

leanprover-community-bot committed 3 years ago

9b11656c

feat(geometry/euclidean/basic): `affine_isometry.angle_map` (#16374)

jsm28 committed 3 years ago

e1d2f5bd

chore(data/nat/part_enat): make `coe_inj` `@[norm_cast]` (#16334)

astrainfinita committed 3 years ago

7fdc06de

feat(order/filter/at_top_bot): add lemmas about convergence of `λ x, r * f x` to `±∞` (#16355)

urkud committed 3 years ago

7ce2bb4a

fix(algebra/category/Module): speedup (#16371)

collares committed 3 years ago

86ee6689

doc(data/nat/{part_enat, lattice}): update doc string (#16345)

astrainfinita committed 3 years ago

075b0d23

feat(analysis/special_functions/stirling): Stirling's formula, part I (#14874)

mo271 committed 3 years ago

a3e847c0

feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281)

YaelDillies committed 3 years ago

e4fb6414

fix(analysis/inner_product_space,geometry/euclidean): two deterministic timeout fixes (#16365)

collares committed 3 years ago

bb0978c2

chore(linear_algebra/*): Lint (#16362)

YaelDillies committed 3 years ago

1cfdf5f3

Older