leanprover-community/mathlib3

Pull Requests Commits

Antoine Chambert-Loir committed 3 years ago

f8b6ea18

patrick's tactic

Antoine Chambert-Loir committed 3 years ago

5f495a0b

with simplifications regarding signature

Antoine Chambert-Loir committed 3 years ago

750ee184

signature and cycle_type

Antoine Chambert-Loir committed 3 years ago

ab9f56a2

Automate Antoine

PatrickMassot committed 3 years ago

ec538300

start simplifying

AntoineChambert-Loir committed 3 years ago

ec2c7dd6

AntoineChambert-Loir committed 4 years ago

d43711cf

garbage avec des vieux restes

AntoineChambert-Loir committed 4 years ago

c0d349d6

Preuve presque finie, quelques sorry

AntoineChambert-Loir committed 4 years ago

ac862c86

AntoineChambert-Loir committed 4 years ago

cd3085ba

cas 1 presque fini

Antoine Chambert-Loir committed 4 years ago

01b0e455

cas 1 presque fini

Antoine Chambert-Loir committed 4 years ago

3a03ae37

AntoineChambert-Loir committed 4 years ago

6003a827

Simplicité de An, preuve calculatoire - init

AntoineChambert-Loir committed 4 years ago

c3f9d1e6

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

Older