Theorem lift.SubfieldWithHom.compat

Modification history

2023-08-25 17:17

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

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

Deleted lift.SubfieldWithHom.compat View on Github →

2023-06-09 23:11

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

feat: port FieldTheory.IsAlgClosed.Basic (#4888)

Added lift.SubfieldWithHom.compat View on Github →