leanprover-community/mathlib

Pull Requests Commits

blocks and primitive actions

Antoine Chambert-Loir committed 3 years ago

74c53f65

style: shorten a line (>100 chars)

Antoine Chambert-Loir committed 4 years ago

b804f5d3

additional corrections which were overlooked in the previous commit

Antoine Chambert-Loir committed 4 years ago

6444a00f

style: implementing suggestions of Eric Wieser

Antoine Chambert-Loir committed 4 years ago

af23e254

the good files, finally

Antoine Chambert-Loir committed 4 years ago

41f90a43

style(src/group_theory/specific_groups/alternating.lean): remove ugly lemmas

Antoine Chambert-Loir committed 4 years ago

d1ca2d4c

style(src/group_theory/iwasawa.lean): put some universal quantifiers into hypotheses

Antoine Chambert-Loir committed 4 years ago

1157ed05

feat(src/group_theory/specific_groups/alternating.lean): prove that the alternating group is perfect

Antoine Chambert-Loir committed 4 years ago

c8651967

style: adjust comment for docstring

Antoine Chambert-Loir committed 4 years ago

5a77a4c8

style: adjust comment for docstring

Antoine Chambert-Loir committed 4 years ago

5eff16da

style: remove some @

Antoine Chambert-Loir committed 4 years ago

d5ef3ac5

style(group_theory/iwasawa.lean): put docstring first

Antoine Chambert-Loir committed 4 years ago

83231db5

style(group_theory/iwasawa.lean): add copyright, remove #print

Antoine Chambert-Loir committed 4 years ago

ab8c6bb3

style (group_theory/iwasawa.lean): shorten proofs and remove unused stuff

Antoine Chambert-Loir committed 4 years ago

86839bc5

style: remove the final #lint

Antoine Chambert-Loir committed 4 years ago

1b0b36f2

feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity

Antoine Chambert-Loir committed 4 years ago

63427df9

feat(measure_theory/group/fundamental_domain): prove equality of integrals (#10448)

urkud committed 4 years ago

b29b9528

feat(measure_theory/integral): dominated convergence for a series (#10398)

urkud committed 4 years ago

563f8c4f

refactor(algebra.abs): Introduce `has_pos_part` and `has_neg_part` classes (#10420)

mans0954 committed 4 years ago

132833b7

feat(linear_algebra/multilinear/basic): multilinear maps with respect to an empty family are all constant (#10433)

ocfnash committed 4 years ago

09b4bfc9

refactor(topology,algebraic_geometry): use bundled maps here and there (#10447)

urkud committed 4 years ago

d487d650

feat(topology/uniform_space/uniform_convergence): slightly generalize theorems (#10444)

urkud committed 4 years ago

3590dc29

feat(topology/sheaves): Generalized some lemmas. (#10440)

erdOne committed 4 years ago

8d07dbf4

chore(ring_theory/polynomial/cyclotomic): use `ratfunc` (#10421)

Vierkantor committed 4 years ago

a086daa5

feat(category_theory/limits): Results about (co)limits in Top (#9985)

erdOne committed 4 years ago

6cb52e67

chore(topology): add 2 missing `inhabited` instances (#10446)

urkud committed 4 years ago

d267b6ca

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

leanprover-community-bot committed 4 years ago

1c001794

feat(measure_theory): TC for smul-invariant measures (#10325)

urkud committed 4 years ago

f578d1d6

feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427)

riccardobrasca committed 4 years ago

0cbba1a4

feat(analysis): derivative of a parametric interval integral (#10404)

urkud committed 4 years ago

c192937f

Older