leanprover-community/mathlib3

Pull Requests Commits

doc(overview): combinatorics section (#5581)

kmill committed 5 years ago

1a39825b

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

eric-wieser committed 5 years ago

5bff8872

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

urkud committed 5 years ago

e0946065

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

sgouezel committed 5 years ago

aa88bb81

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

kbuzzard committed 5 years ago

a7d05c45

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

adomani committed 5 years ago

12b5024b

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

urkud committed 5 years ago

fceb7c1a

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

alexjbest committed 5 years ago

e142c825

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

bryangingechen committed 5 years ago

e35a703f

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

adamtopaz committed 5 years ago

f5f879e2

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

urkud committed 5 years ago

9f6300e9

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

awainverse committed 5 years ago

9d3c05ad

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

kbuzzard committed 5 years ago

afc3f03a

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

urkud committed 5 years ago

d94f0a27

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

urkud committed 5 years ago

409ea425

chore(data/fintype/card): generalize `equiv.prod_comp` to `function.bijective.prod_comp` (#5551)

urkud committed 5 years ago

06a11fd5

feat(analysis/normed_space/inner_product): upgrade orthogonal projection to a continuous linear map (#5543)

hrmacbeth committed 5 years ago

ea3815fb

feat(algebra/big_operators/nat_antidiagonal): add prod_antidiagonal_eq_prod_range_succ (#5528)

kbuzzard committed 5 years ago

b57d562c

feat(data/fin): there is at most one `order_iso` from `fin n` to `α` (#5499)

urkud committed 5 years ago

c32efeae

chore(*): golf some proofs (#5548)

urkud committed 5 years ago

8aa23326

chore(data/real/cau_seq): golf some proofs (#5545)

urkud committed 5 years ago

e0030ffe

chore(linear_algebra/basic): notation for span of a singleton (#5538)

hrmacbeth committed 5 years ago

b542cfbc

doc(lint/type_classes): add has_coe_to_fun linter (#5546)

fpvandoorn committed 5 years ago

fcbaf625

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

leanprover-community-bot committed 5 years ago

d2bde119

feat(logic/basic): exists_unique_false simp lemma (#5544)

pechersky committed 5 years ago

54bf708d

refactor(analysis/analytic/basic): redefine `formal_multilinear_series.radius` (#5349)

urkud committed 5 years ago

0830bfd4

chore(analysis/normed_space/inner_product): notation for orthogonal complement (#5536)

hrmacbeth committed 5 years ago

10f6c151

feat(field_theory/galois): is_galois.tfae (#5542)

tb65536 committed 5 years ago

cca63650

chore(algebra): move lemmas from ring_theory.algebra_tower to algebra.algebra.tower (#5506)

kckennylau committed 5 years ago

b04aeb5e

feat(data/tprod): finite products of types (#5385)

fpvandoorn committed 5 years ago

a40f31fb

Newer Older