leanprover-community/mathlib3

Pull Requests Commits

remove decidable instance

abentkamp committed 3 years ago

ed75b7a6

abentkamp committed 3 years ago

09b4a9ec

abentkamp committed 3 years ago

724d7c16

abentkamp committed 3 years ago

10104705

feat(data/int/log): integer logarithms of linearly ordered fields (#13913)

eric-wieser committed 3 years ago

ba1c3f36

feat(topology/vector_bundle): use trivialization.symm to simplify the product of vector bundles (#14361)

fpvandoorn committed 3 years ago

f8d5c649

feat(measure_theory/function/conditional_expectation): Conditional expectation of an indicator (#14058)

RemyDegenne committed 3 years ago

660918bb

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

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

feat(probability/strong_law): the strong law of large numbers (#13690)

sgouezel committed 3 years ago

0973ad45

feat(field_theory/finite/galois_field): Finite fields are Galois (#14290)

tb65536 committed 3 years ago

0d14ee8b

Older