Commit 2023-08-25 17:17 89776af8

View on Github →

chore(IsAlgClosed): move some defs about lift into IsAlgClosed namespace (#6754)

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.lift.SubfieldWithHom.compat

added theorem IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom

added theorem IsAlgClosed.lift.SubfieldWithHom.le_def

added theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top

added theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal

added theorem IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded

added structure IsAlgClosed.lift.SubfieldWithHom

deleted theorem lift.SubfieldWithHom.compat

deleted theorem lift.SubfieldWithHom.exists_maximal_subfieldWithHom

deleted theorem lift.SubfieldWithHom.le_def

deleted theorem lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top

deleted theorem lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal

deleted theorem lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded

deleted structure lift.SubfieldWithHom