leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 4 years ago

Verified d7866a64

b-mehta committed 4 years ago

Verified f68d7df9

b-mehta committed 4 years ago

Verified 9233eea6

agusakov committed 4 years ago

Verified 932e6c6d

feat(measure_theory/pi): finite products of measures (#5414)

fpvandoorn committed 4 years ago

0837fc30

feat(data/equiv/basic): rfl lemma for equiv_congr (#5585)

pechersky committed 4 years ago

e3501142

feat(combinatorics/simple_graph): finitely many simple graphs on a finite type (#5584)

b-mehta committed 4 years ago

57c6d191

feat(data/finset/basic): add `finset.piecewise_le_piecewise` (#5572)

urkud committed 4 years ago

9fc7aa56

chore(data/prod): add `prod.forall'` and `prod.exists'` (#5570)

urkud committed 4 years ago

0a4fbd8c

feat(data/nat/fib): fib n is a strong divisibility sequence (#5555)

Hanting Zhang committed 4 years ago

0dc7a27c

chore(data/finset/sort): upgrade `finset.mono_of_fin` to an `order_iso` (#5495)

urkud committed 4 years ago

9f252442

feat(linear_algebra/alternating): Show the link to linear_independent (#5477)

eric-wieser committed 4 years ago

9ea7e462

feat(group_theory/dihedral): add dihedral groups (#5171)

shingtaklam1324 committed 4 years ago

04f8fd74

doc(overview): pluralization convention (#5583)

kmill committed 4 years ago

ee2c963e

doc(overview): Add alternating_map (#5582)

eric-wieser committed 4 years ago

e6982901

doc(overview): combinatorics section (#5581)

kmill committed 4 years ago

1a39825b

doc(overview): add missing algebras to overview (#5579)

eric-wieser committed 4 years ago

5bff8872

chore(topology/algebra/ordered,analysis/specific_limits): two more limits (#5573)

urkud committed 4 years ago

e0946065

feat(measure_theory/borel_space): the inverse of a closed embedding is measurable (#5567)

sgouezel committed 4 years ago

aa88bb81

chore(number_theory/bernoulli): refactor definition of bernoulli (#5534)

kbuzzard committed 4 years ago

a7d05c45

feat(data/polynomial/erase_lead): add lemma erase_lead_card_support_eq (#5529)

adomani committed 4 years ago

12b5024b

chore(algebra/group,algebra/group_with_zero): a few more injective/surjective constructors (#5547)

urkud committed 4 years ago

fceb7c1a

feat(algebra/group/prod) Units of a product monoid (#5563)

alexjbest committed 4 years ago

e142c825

feat(algebra/ordered_{group,field}): more lemmas relating inv and mul inequalities (#5561)

bryangingechen committed 4 years ago

e35a703f

feat(linear_algebra/dimension): linear equiv iff eq dim (#5559)

adamtopaz committed 4 years ago

f5f879e2

chore(data/complex/basic): upgrade `complex.norm_sq` to a `monoid_with_zero_hom` (#5553)

urkud committed 4 years ago

9f6300e9

feat(ring_theory/simple_module): simple modules and Schur's Lemma (#5473)

awainverse committed 4 years ago

9d3c05ad

feat(algebra/ordered_group): add linear_ordered_comm_group and linear_ordered_cancel_comm_monoid (#5286)

kbuzzard committed 4 years ago

afc3f03a

chore(data/list): a list sorted w.r.t. `(<)` has no duplicates (#5550)

urkud committed 4 years ago

d94f0a27

chore(algebra/*): move some lemmas to `div_inv_monoid` (#5552)

urkud committed 4 years ago

409ea425

Older