leanprover-community/mathlib

Pull Requests Commits

b-mehta committed 2 years ago

6c7911ec

b-mehta committed 3 years ago

b9a8c929

b-mehta committed 3 years ago

8a710a7a

b-mehta committed 3 years ago

f0a9a94b

b-mehta committed 3 years ago

a646fa7c

b-mehta committed 3 years ago

38478f93

b-mehta committed 3 years ago

7eec5bdc

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

feat(group_theory/schreier): A theorem of Schur: A group with finitely many commutators has finite commutator subgroup (#17311)

tb65536 committed 3 years ago

91ce9cbd

chore: freeze logic.relation (#17573)

kbuzzard committed 3 years ago

71dbd401

feat(algebra/ne_zero): generalize lemmas (#17477)

astrainfinita committed 3 years ago

bb168510

refactor(*): scrub imports (#17568)

kim-em committed 3 years ago

70fd9563

fix(tactic/choose): typo (#17552)

fzyzcjy committed 3 years ago

fd47bdf0

feat(ring_theory/polynomial/cyclotomic): generalize some lemmas to `[ring R]` (#17555)

urkud committed 3 years ago

83490903

feat(data/list/join): add `list.append_join_append` and `list.reverse_join` (#17554)

madvorak committed 3 years ago

c34a1aa4

chore(*): golf (#17558)

urkud committed 3 years ago

17a9f8f7

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

j-loreaux committed 3 years ago

7cca1710

chore(topology/algebra/order/basic): move field-parts into new file (#17549)

mcdoll committed 3 years ago

49ae0e37

feat(data/set/prod): Preimage of `set.pi` (#17534)

YaelDillies committed 3 years ago

1955c1cf

Older