Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lift.subfield_with_hom.le_def

Modification history

2021-09-16 10:37
src/field_theory/algebraic_closure.lean
feat(field_theory/algebraic_closure): map from algebraic extensions into the algebraic closure (#9110)
Added lift.subfield_with_hom.le_defView on Github →