leanprover-community/mathlib3

Pull Requests Commits

feat(linear_algebra/basis): add lemmas (#17606)

riccardobrasca committed 3 years ago

cf1f8bcb

feat(combinatorics/simple_graph/acyclic): acyclic graphs and trees (#17213)

kmill committed 3 years ago

b0768801

refactor(category_theory): reduce imports (#17545)

kim-em committed 3 years ago

e83fa832

chore(ring_theory): move `submodule.fg` to `ring_theory.finiteness` (#17541)

Vierkantor committed 3 years ago

25cf7631

chore(*): various simplifications (#17597)

Ruben-VandeVelde committed 3 years ago

8350c34a

chore(*): add mathlib4 synchronization labels (#17596)

j-loreaux committed 3 years ago

74b4ee12

chore(algebra/order/ring/defs): make `strict_ordered_ring.to_ordered_ring'` choice-free (#17563)

astrainfinita committed 3 years ago

4ef6708b

chore(algebra/order/ring): rename `.../nontrivial` to `.../char_zero` (#17562)

astrainfinita committed 3 years ago

bc2f30ca

chore(order/bounded_order): lemmas about disjoint on prod, pi, and Prop (#17500)

eric-wieser committed 3 years ago

8f654ad4

chore(number_theory/bernoulli_polynomials): tidy docs (#16705)

ericrbg committed 3 years ago

ca3d21f7

feat(algebra/category/FinVect): generalize to fgModule (#13962)

kim-em committed 3 years ago

19a70dce

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

leanprover-community-bot committed 3 years ago

76702385

chore(logic/pairwise): freeze (#17589)

mcdoll committed 3 years ago

874f7f18

chore(data/pnat/defs): freeze (#17582)

Ruben-VandeVelde committed 3 years ago

ab8f1cfa

chore(scripts/port_status): avoid assignment expression (#17581)

Ruben-VandeVelde committed 3 years ago

b7b1590e

feat(combinatorics/quiver/*) Notation for prefunctors (#17576)

bottine committed 3 years ago

c6dd521e

refactor(data/fintype/basic): split file (#17578)

kim-em committed 3 years ago

c3019c79

feat(category_theory/morphism_property): (In/Sur/Bi)jective as morphism properties (#17592)

erdOne committed 3 years ago

7f963633

feat(group_theory/index): Add `iff`-lemmas `relindex_eq_one` and `card_eq_one` (#17271)

tb65536 committed 3 years ago

c00ed312

feat(data/set/intervals/disjoint): Add 4 lemmas about unions of closed semi-infinite intervals. (#17587)

kkytola committed 3 years ago

1330a700

fix(linear_algebra/affine_space/affine_subspace): remove obsolete comment (#17586)

jsm28 committed 3 years ago

ee768c0f

feat(combinatorics/simple_graph/basic): Graph construction from edges (#16691)

VArtem committed 3 years ago

8ab239e9

chore(algebra/pempty_instances): freeze file (#17579)

riccardobrasca committed 3 years ago

bef2305b

feat(order/cover): Covby iff Ioo empty (#17567)

MadPidgeon committed 3 years ago

6d29b2c8

chore(topology/{fiber,vector}_bundle/*): reorganize files (#17559)

hrmacbeth committed 3 years ago

87f3aec4

feat(measure_theory/integral): substitution without continuity at endpoints (#17540)

loefflerd committed 3 years ago

0d4bacdc

feat(measure_theory/constructions/pi): Right invariance of the product measure (#17518)

YaelDillies committed 3 years ago

1f93ad3e

feat(measure_theory/integral): integral composed with smul (#17455)

sgouezel committed 3 years ago

f087f43d

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575)

eric-wieser committed 3 years ago

17ef379e

feat(topology/subset_properties): Add `is_clopen.preimage` (#17469)

jlcbrown committed 3 years ago

720aee9e

Older