leanprover-community/mathlib3

Pull Requests Commits

adomani committed 3 years ago

d79872fd

Merge branch 'master' into adomani_nuovo

adomani committed 3 years ago

fa2360bb

feat(measure_theory/integral): add formulas for average over an interval (#14132)

urkud committed 3 years ago

5da37314

feat(data/set/finite): set priority for fintype_insert' and document (#14363)

kmill committed 3 years ago

c1e21212

feat(group_theory/subgroup/basic): `zpowers_eq_bot` (#14366)

tb65536 committed 3 years ago

f5822984

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

adomani committed 3 years ago

faad8bc1

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

Merge branch 'adomani_ptl' into adomani_coeff_previous_power

adomani committed 3 years ago

09f3c908

adomani committed 3 years ago

363804e6

adomani committed 3 years ago

31b860d7

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

Merge branch 'adomani_ptl' into adomani_coeff_previous_power

adomani committed 3 years ago

24d90e42

trimmed version

adomani committed 3 years ago

727591e1

commented out unused lemmas

adomani committed 3 years ago

289aa215

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

khwilson committed 3 years ago

533c67bc

Merge branch 'master' into adomani_ptl

adomani committed 3 years ago

2912a36b

Older