Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-03 14:17 324d845a

View on Github →

feat(field_theory/krull_topology): defined Krull topology on Galois groups (#11780)

Estimated changes

Created src/field_theory/krull_topology.lean

added theorem finite_dimensional_sup

added def finite_exts

added def fixed_by_finite

added def gal_basis

added def gal_group_basis

added theorem intermediate_field.finite_dimensional_bot

added theorem intermediate_field.fixing_subgroup.antimono

added theorem intermediate_field.fixing_subgroup.bot

added theorem intermediate_field.map_id

added theorem intermediate_field.map_mono

added theorem mem_fixing_subgroup_iff

added theorem mem_gal_basis_iff

added theorem top_fixed_by_finite