Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alg_hom.coe_field_range

Modification history

2022-08-17 22:03
src/field_theory/intermediate_field.lean
feat(field_theory/intermediate_field): Add `alg_hom.field_range` (#16078) …
Added alg_hom.coe_field_rangeView on Github →