Commit 2023-06-17 08:04 afa4bb08

View on Github →

feat: port FieldTheory.KrullTopology (#5170)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/KrullTopology.lean

added theorem IntermediateField.finiteDimensional_bot

added theorem IntermediateField.fixingSubgroup.antimono

added theorem IntermediateField.fixingSubgroup.bot

added theorem IntermediateField.fixingSubgroup_isClosed

added theorem IntermediateField.fixingSubgroup_isOpen

added theorem IntermediateField.map_id

added theorem IntermediateField.map_mono

added theorem IntermediateField.mem_fixingSubgroup_iff

added theorem finiteDimensional_sup

added def finiteExts

added def fixedByFinite

added def galBasis

added def galGroupBasis

added theorem krullTopology_t2

added theorem krullTopology_totallyDisconnected

added theorem mem_galBasis_iff

added theorem top_fixedByFinite