leanprover-community/mathlib3

Pull Requests Commits

adomani committed 3 years ago

363804e6

trimmed version

adomani committed 3 years ago

727591e1

commented out unused lemmas

adomani committed 3 years ago

289aa215

Merge branch 'master' into adomani_ptl

adomani committed 3 years ago

2912a36b

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

feat(measure_theory): use `pseudo_metrizable_space` instead of `metrizable_space` (#14310)

urkud committed 3 years ago

542d06a6

refactor(category_theory/shift_functor): improve defeq of inverse (#14300)

kim-em committed 3 years ago

c100004c

chore(topology/separation): golf some proofs (#14279)

urkud committed 3 years ago

56de25ef

Older