leanprover-community/mathlib

Pull Requests Commits

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

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

Newer Older