mathlib3
feat(field_theory/krull_topology): `alg_hom_of_ultrafilter`
#13307

Open

feat(field_theory/krull_topology): `alg_hom_of_ultrafilter` #13307

Sebastian-Monnet wants to merge 79 commits into master from alg_hom_of_ultrafilter

added alg_hom_of_ultrafilter

b0bbac9b

fixed curly braces

20a8e229

Sebastian-Monnet added awaiting-review

Vierkantor changed the title ~~added alg_hom_of_ultrafilter~~ feat(field_theory/krull_topology): added alg_hom_of_ultrafilter 3 years ago

jcommelin commented on 2022-04-14

jcommelin removed awaiting-review

jcommelin added awaiting-author

Update src/field_theory/krull_topology.lean

1d6c60e0

Update src/field_theory/krull_topology.lean

7a34e3a6

Update src/field_theory/krull_topology.lean

9a095c20

Update src/field_theory/krull_topology.lean

e13c48f6

moved some things to ultrafilter file

cf805b8f

renamed lemma

ecc51ed2

moved map_pure to ultrafilter

2aac7dde

Sebastian-Monnet removed awaiting-author

Sebastian-Monnet added awaiting-review

jcommelin commented on 2022-04-21

jcommelin removed awaiting-review

jcommelin added awaiting-author

Update src/order/filter/ultrafilter.lean

7403f22b

Update src/field_theory/krull_topology.lean

19073b0c

Update src/field_theory/krull_topology.lean

b61d00f4

Update src/field_theory/krull_topology.lean

46994229

Update src/field_theory/krull_topology.lean

96fb4a48

Update src/field_theory/krull_topology.lean

73ad1c48

Update src/field_theory/krull_topology.lean

4bbc128e

shorter proof of ultrafilter.map_map

eabb6287

Sebastian-Monnet removed awaiting-author

Sebastian-Monnet added awaiting-review

jcommelin commented on 2022-04-25

YaelDillies changed the title ~~feat(field_theory/krull_topology): added alg_hom_of_ultrafilter~~ feat(field_theory/krull_topology): `alg_hom_of_ultrafilter` 3 years ago

Update src/order/filter/ultrafilter.lean

a1ba69a8

YaelDillies added review-in-progress

golf

f9953290

YaelDillies commented on 2022-04-25

YaelDillies removed review-in-progress

YaelDillies commented on 2022-04-25

jcommelin removed awaiting-review

jcommelin added awaiting-author

leanprover-community-bot-assistant added blocked-by-other-PR

leanprover-community-bot-assistant removed blocked-by-other-PR

Merge remote-tracking branch 'origin/master' into alg_hom_of_ultrafilter

7972c341

bump inclusion_mk

33c06bf8

Sebastian-Monnet removed awaiting-author

Sebastian-Monnet added awaiting-review

golf and move

da0ec8e3

golf further

9ff9e9f5

jcommelin commented on 2022-05-04

jcommelin removed awaiting-review

jcommelin added awaiting-author

added proof of profiniteness

76a0f197

fixed curly braces

edabe72a

fixed curly braces

ddad7c45

Sebastian-Monnet removed awaiting-author

Sebastian-Monnet added awaiting-review

pulled fields out into variables

74d047da

changed line spacing

b453a429

Merge remote-tracking branch 'origin/master' into alg_hom_of_ultrafilter

618aaab2

fixed linter issues

3bacf950

fixed linter issues

78a315aa

fixed linter issue

ceed55f1

removed all h_splits assumptions

9989c913

golfing

24e5f739

renamed and moved lemma about adjoining finite sets of algebraic elem…

9fc34648

moved intermediate_field.adjoin.finite_dimensional_of_finite_set to p…

3f8ab188

fixed line length

cbfaf48d

changed API from ultrafilters on equivalences to ultrafilters on alge…

24fa390a

changed names to be more specific

ace76e81

changed name of lemma about limit of ultrafilter actually being a limit

e0e651f8

tb65536 commented on 2022-05-23

Update src/field_theory/krull_topology.lean

24f6846a

Update src/field_theory/krull_topology.lean

39ed2347

Update src/field_theory/krull_topology.lean

a6cb0189

tb65536 commented on 2022-05-24

Update src/field_theory/krull_topology.lean

6174456f

Update src/field_theory/krull_topology.lean

bd847cf8

Update src/field_theory/krull_topology.lean

6bdc154e

fixed indentation

0323aecf

tb65536 commented on 2022-05-24

Update src/field_theory/krull_topology.lean

8360fa7c

Update src/field_theory/krull_topology.lean

4f2511be

tb65536 commented on 2022-05-24

tb65536 commented on 2022-05-25

Update src/field_theory/krull_topology.lean

66973042

Update src/field_theory/krull_topology.lean

235ff036

Update src/field_theory/krull_topology.lean

fa869f4d

tb65536 commented on 2022-05-26

Update src/field_theory/krull_topology.lean

29a0803f

tb65536 commented on 2022-05-29

Update src/field_theory/krull_topology.lean

f62900ac

Update src/field_theory/krull_topology.lean

cdedc6e6

Update src/field_theory/krull_topology.lean

15627577

Update src/field_theory/krull_topology.lean

d69031d1

Update src/field_theory/krull_topology.lean

4d6b7ff2

tb65536 commented on 2022-05-29

Update src/field_theory/krull_topology.lean

1487fe71

Update src/field_theory/krull_topology.lean

d11b3571

tb65536 commented on 2022-05-30

Update src/field_theory/krull_topology.lean

5cb6da2f

kbuzzard approved these changes on 2022-06-27

Update src/field_theory/krull_topology.lean

b534dc1a

fixed docstrings

5546277a

Merge branch 'alg_hom_of_ultrafilter' of https://github.com/leanprove…

3dbe706b

ghost added blocked-by-other-PR

Merge branch 'master' into alg_hom_of_ultrafilter

a9e43730

Update ultrafilter.lean

9cfe121f

eric-wieser commented on 2022-07-13

Merge remote-tracking branch 'origin/master' into alg_hom_of_ultrafilter

804c4660

fix a previous bad merge

609fc302

remove unused lemma from another PR

4307e385

eric-wieser removed blocked-by-other-PR

ghost deleted a comment from leanprover-community-bot-assistant on 2022-07-14

eric-wieser commented on 2022-07-14

Update src/field_theory/krull_topology.lean

969f0ef6

put arguments on one line

99ffb64e

changed to nhds syntax

802cd58c

Merge branch 'alg_hom_of_ultrafilter' of https://github.com/leanprove…

35676b88

eric-wieser commented on 2022-07-14

changed from intermediate_field to is_scalar_tower

a59c802d

changed definition of ultrafilter.glued_generators_of_pushforwards_fu…

c92b376b

eric-wieser commented on 2022-07-23

fixed indentation

e7c275b0

eric-wieser commented on 2022-07-23

Update src/field_theory/krull_topology.lean

dbb4b469

eric-wieser commented on 2022-07-24

Update src/field_theory/krull_topology.lean

c4892c4f

Update src/field_theory/adjoin.lean

6216f91e

jcommelin commented on 2022-09-02

jcommelin removed awaiting-review

jcommelin added awaiting-author

kim-em added too-late

Reviewers

kbuzzard

jcommelin

eric-wieser

YaelDillies

tb65536

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone

mathlib3 feat(field_theory/krull_topology): `alg_hom_of_ultrafilter` #13307 Open

feat(field_theory/krull_topology): `alg_hom_of_ultrafilter` #13307

mathlib3
feat(field_theory/krull_topology): `alg_hom_of_ultrafilter`
#13307

Open