leanprover-community/mathlib

Pull Requests Commits

update doc-string for Bhavik's example

adomani committed 4 years ago

1a39c318

add Eric's version of the lemma

adomani committed 4 years ago

de003bdb

update doc-string, following Sébastien's comment

adomani committed 4 years ago

ead32cb6

adomani committed 4 years ago

dd3548e3

Merge branch 'master' into counterexamples

adomani committed 4 years ago

e4b9655a

feat(algebra/lie/weights): define weight spaces of Lie modules (#7537)

ocfnash committed 4 years ago

132328c4

feat(topology/subset_properties, homeomorph): lemmata about embeddings (#7431)

AlexKontorovich committed 4 years ago

4a8a5950

feat(algebraic_geometry/structure_sheaf): Structure sheaf on basic opens (#7405)

justus-springer committed 4 years ago

583ad823

feat(topology/category/*): Add alternative explicit limit cones for `Top`, etc. and shows `X : Profinite` is a limit of finite sets. (#7448)

adamtopaz committed 4 years ago

dbcd4546

feat(group_theory/perm/*): lemmas about `extend_domain`, `fin_rotate`, and `fin.cycle_type` (#7447)

awainverse committed 4 years ago

515fb2f0

feat(ring_theory/hahn_series): order of a nonzero Hahn series, reindexing summable families (#7444)

awainverse committed 4 years ago

5cfcb6a0

feat(topology/uniform_space): is_closed_of_spread_out (#7538)

PatrickMassot committed 4 years ago

72e151d8

feat(group_theory.quotient_group): add eq_iff_div_mem (#7523)

riccardobrasca committed 4 years ago

301542a4

feat(field_theory/polynomial_galois_group): More flexible version of gal_action_hom_bijective_of_prime_degree (#7508)

tb65536 committed 4 years ago

63a17823

feat(data/nat/cast): pi.coe_nat and pi.nat_apply (#7492)

jcommelin committed 4 years ago

565310f1

feat(algebra/module/basic): smul_add_hom_one (#7461)

jcommelin committed 4 years ago

190d4e28

feat(category_theory/arrow): arrow.mk_inj (#7456)

jcommelin committed 4 years ago

91d5aa6b

refactor(*): more choice-free proofs (#7455)

digama0 committed 4 years ago

6fc8b2a9

feat(group_theory/solvable): S_5 is not solvable (#7453)

tb65536 committed 4 years ago

dec29aa3

refactor(group_theory/perm/*): disjoint and support in own file (#7450)

pechersky committed 4 years ago

95b91b38

feat(ring_theory/finiteness): add monoid_algebra.ft_iff_fg (#7445)

riccardobrasca committed 4 years ago

251a42b5

feat(linear_algebra/quadratic_form): provide `distrib_mul_action S (quadratic_form M R)` when `S` has no addition. (#7443)

eric-wieser committed 4 years ago

be1af7ce

feat(algebra/monoid_algebra): add add_monoid_algebra_ring_equiv_direct_sum (#7422)

eric-wieser committed 4 years ago

5d873a65

refactor(polynomial/*): make polynomials irreducible (#7421)

sgouezel committed 4 years ago

3a5c8711

feat(finset/basic): downward induction for finsets (#7379)

YaelDillies committed 4 years ago

322ccc54

feat(order/closure): closure of unions and bUnions (#7361)

YaelDillies committed 4 years ago

11a06de1

feat(order/well_founded_set): Higman's Lemma (#7212)

awainverse committed 4 years ago

b20e6647

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

leanprover-community-bot committed 4 years ago

cd5864f3

ci(.github/workflows/{build,dependent-issues}.yml): auto-cancel workflows on previous commits (#7536)

bryangingechen committed 4 years ago

6a7ddcc2

ci(.github/workflows/build.yml): switch to trepplein (#7532)

gebner committed 4 years ago

93f9b3de

Older