leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into CDGA_challenge2

kim-em committed 3 years ago

5d8a54b0

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

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

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

feat(combinatorics/simple_graph/regularity/energy): Energy of a partition (#12958)

YaelDillies committed 3 years ago

523d1779

feat(algebra/algebra/unitization): define unitization of a non-unital algebra (#12601)

j-loreaux committed 3 years ago

50903f0d

chore(ring_theory/valuation/basic): fix valuation_apply (#13045)

mariainesdff committed 3 years ago

119eb05e

feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043)

Vierkantor committed 3 years ago

e4c64493

feat(algebra/algebra/tower): `span A s = span R s` if `R → A` is surjective (#13042)

Vierkantor committed 3 years ago

9aec6df4

Older