leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into bicategory-coherence-tactic

yuma-mizuno committed 3 years ago

e69007d9

feat(algebraic_topology): map_alternating_face_map_complex (#13028)

joelriou committed 3 years ago

c2339caa

feat(combinatorics/simple_graph/regularity/bound): Numerical bounds for Szemerédi's regularity lemma (#12962)

YaelDillies committed 3 years ago

8a213165

feat(combinatorics/simple_graph/uniform): Graph uniformity and uniform partitions (#12957)

YaelDillies committed 3 years ago

299984b4

feat(linear_algebra/matrix): any matrix power can be expressed as sums of powers `0 ≤ k < fintype.card n` (#12983)

eric-wieser committed 3 years ago

47b1d786

chore(data/finset/card): add `card_disj_union` (#13061)

eric-wieser committed 3 years ago

fc35cb32

feat(topology/sets/order): Clopen upper sets (#12670)

YaelDillies committed 3 years ago

7f450cb8

yuma-mizuno committed 3 years ago

87f95660

yuma-mizuno committed 3 years ago

9b43a390

yuma-mizuno committed 3 years ago

4e9b8d56

split a function into monoidal and bicategorical cases

yuma-mizuno committed 3 years ago

aca6b690

feat(topology): add lemmas about `frontier` (#13054)

urkud committed 3 years ago

518e81a8

chore(data/set/pointwise): Golf using `set.image2` API (#13051)

YaelDillies committed 3 years ago

de62b061

feat(analysis/special_functions/pow): abs value of real to complex power (#13048)

loefflerd committed 3 years ago

25e8730e

feat(data/fin): lemmas about ordering and cons (#13044)

eric-wieser committed 3 years ago

33a323cd

fix(tactic/generalize_proofs): instantiate mvars (#13025)

digama0 committed 3 years ago

644a848d

feat(data/polynomial/erase_lead): add two erase_lead lemmas (#12910)

adomani committed 3 years ago

af3911c1

feat(analysis/locally_convex): polar sets for dualities (#12849)

mcdoll committed 3 years ago

e31f0319

Merge branch 'master' into bicategory-coherence-tactic

yuma-mizuno committed 3 years ago

ed1a3b34

chore(*): sort out some to_additive and simp orderings (#13038)

alexjbest committed 3 years ago

f13ee544

feat(ring_theory/graded_algebra): define homogeneous localisation (#12784)

jjaassoonn committed 3 years ago

37a8a0b2

feat(algebra/associates): add two instances and a lemma about the order on the monoid of associates of a monoid (#12863)

Paul-Lez committed 3 years ago

cdd1703c

fix(data/fintype/basic): generalize fintype instance for fintype.card_coe (#13055)

kmill committed 3 years ago

cd51f0de

chore(*): removing some `by { dunfold .., apply_instance }` proofs (#13050)

mcdoll committed 3 years ago

f2fd6db6

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

leanprover-community-bot committed 3 years ago

ca3bb9ef

feat(measure_theory/*): refactor integral to allow non second-countable target space (#12942)

sgouezel committed 3 years ago

fc758559

feat(linear_algebra/dual): define the algebraic dual pairing (#12827)

mcdoll committed 3 years ago

d28a163e

feat(algebra/ring/basic): neg_zero for distrib_neg (#13049)

ericrbg committed 3 years ago

c594e2b9

feat(set_theory/cardinal): bit lemmas for exponentiation (#13010)

vihdzp committed 3 years ago

b446c498

fix(tactic/norm_num): make norm_num user command match norm_num better (#12667)

kmill committed 3 years ago

92b29c77

Older