leanprover-community/mathlib

Pull Requests Commits

winston-h-zhang committed 3 years ago

93c7d890

delete subspace file

winston-h-zhang committed 3 years ago

e61d71b2

winston-h-zhang committed 3 years ago

271c74ab

winston-h-zhang committed 3 years ago

4e8477f9

winston-h-zhang committed 3 years ago

baf9c8e6

winston-h-zhang committed 3 years ago

e3dcaff9

winston-h-zhang committed 3 years ago

fd5a3f84

winston-h-zhang committed 3 years ago

9649cefb

winston-h-zhang committed 3 years ago

42683d16

winston-h-zhang committed 3 years ago

8b31897c

delete accidentally copied artifacts

winston-h-zhang committed 3 years ago

c149e870

winston-h-zhang committed 3 years ago

6fa3638d

chore(set_theory/surreal/basic): clarify some proofs (#14356)

Ruben-VandeVelde committed 3 years ago

ebb52066

refactor(analysis/normed_space/pi_Lp): golf some instances (#14339)

urkud committed 3 years ago

cdaa6d2b

fix(topology/vector_bundle): squeeze simp, remove non-terminal simp (#14357)

fpvandoorn committed 3 years ago

23f30a30

feat(topology/local_homeomorph): define helper definition (#14360)

fpvandoorn committed 3 years ago

88f8de36

refactor(logic/equiv/set): open set namespace (#14355)

fpvandoorn committed 3 years ago

483b54f1

chore(data/list/forall2): fix incorrect docstring (#14276)

b-mehta committed 3 years ago

ec8587f4

feat(linear_algebra/bilinear_form): generalize scalar instances, fix diamonds (#14358)

eric-wieser committed 3 years ago

73a61259

refactor(algebra/direct_sum/basic): use the new polymorphic subobject API (#14341)

eric-wieser committed 3 years ago

28f7172e

feat(analysis/convolution): the predicate `convolution_exists` (#13541)

fpvandoorn committed 3 years ago

a07493af

doc(100.yaml): add Law of Large Numbers (#14353)

fpvandoorn committed 3 years ago

dc22d65a

feat(category_theory/comm_sq): functors mapping pullback/pushout squares (#14351)

kim-em committed 3 years ago

9d193c59

feat(linear_algebra/tensor_power): Add notation for tensor powers, and a definition of multiplication (#14196)

eric-wieser committed 3 years ago

53a70a08

feat(representation_theory/invariants): average_map is a projection onto the subspace of invariants (#14167)

antoinelab01 committed 3 years ago

8e3deffc

feat(group_theory/index): Lemmas for when `relindex` divides `index` (#14314)

tb65536 committed 3 years ago

893f4800

feat(linear_algebra/quadratic_form/isometry): extract from `linear_algebra/quadratic_form/basic` (#14305)

eric-wieser committed 3 years ago

65f1f8e2

chore(order/bounded_order): Golf `disjoint` API (#14194)

YaelDillies committed 3 years ago

9870d138

feat(analysis/sum_integral_comparisons): Comparison lemmas between finite sums and integrals (#13179)

khwilson committed 3 years ago

533c67bc

feat(measure_theory/integral/integral_eq_improper): Covering finite intervals by finite intervals (#13514)

khwilson committed 3 years ago

93df724a

Older