leanprover-community/mathlib

Pull Requests Commits

maybe this is useful, for many lemmas we otherwise generate too many useless simp lemmas

fpvandoorn committed 3 years ago

6417fad0

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

feat(category_theory/preadditive): hom orthogonal families (#13871)

kim-em committed 3 years ago

179ae9e8

chore(set_theory/ordinal/*): improve autogenerated instance names for `o.out.α` (#14342)

vihdzp committed 3 years ago

c340170b

feat(set_theory/game/basic): mul_cases lemmas (#14343)

vihdzp committed 3 years ago

10f415ad

feat(set_theory/surreal/basic): ordinals are numeric (#14325)

vihdzp committed 3 years ago

dc363338

feat(ring_theory/unique_factorization_domain): misc lemmas on factors (#14333)

Vierkantor committed 3 years ago

59ef0700

feat(set_theory/cardinal/basic): Inline instances (#14130)

vihdzp committed 3 years ago

3f0a2bb4

feat(topology/uniform_space/uniform_convergence): Uniform Cauchy sequences (#14003)

khwilson committed 3 years ago

b3ff79ae

refactor(topology/sequences): rename some `sequential_` to `seq_` (#14318)

urkud committed 3 years ago

dab06b6b

feat(group_theory/sylow): The number of sylow subgroups is indivisible by p (#14313)

tb65536 committed 3 years ago

bbf57768

feat(probability/stopping): measurability of comparisons of stopping times (#14061)

RemyDegenne committed 3 years ago

7a6d8505

feat(data/set/function): add `monotone_on.monotone` etc (#14301)

urkud committed 3 years ago

8df8968c

feat(ring_theory/power_series): Added lemmas regarding rescale (#14283)

laughinggas committed 3 years ago

33262e0c

feat(topology/vector_bundle): define pretrivialization.symm (#14192)

fpvandoorn committed 3 years ago

15e8bc48

refactor(data/set/finite): reorganize and put emphasis on fintype instances (#14136)

kmill committed 3 years ago

2b35fc7b

chore(linear_algebra/quadratic_form/basic): Reorder lemmas (#14326)

eric-wieser committed 3 years ago

34e450b1

feat(algebra/ne_zero): add helper methods (#14286)

ericrbg committed 3 years ago

275dd0f3

feat(linear_algebra/tensor_algebra/basic): add `tensor_algebra.tprod` (#14197)

eric-wieser committed 3 years ago

15f49ae2

feat(linear_algebra/affine_space/affine_equiv): extra lemmas and docstrings (#14319)

eric-wieser committed 3 years ago

9288a2d9

chore(measure_theory/function/l1_space): drop `integrable.sub'` (#14309)

urkud committed 3 years ago

aa6dc575

feat(linear_algebra/trace): trace of transpose map (#13897)

antoinelab01 committed 3 years ago

2962eabc

feat(category_theory/limits): pullback squares (#14220)

kim-em committed 3 years ago

b5128b8a

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

leanprover-community-bot committed 3 years ago

94644b7d

Older