Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 22:03 26c2c38d

View on Github →

feat(field_theory/intermediate_field): Add alg_hom.field_range (#16078) This PR adds alg_hom.field_range (which produces an intermediate_field rather than a subalgebra) and copies over the API from ring_hom.field_range (which produces a subfield rather than a subring).

Estimated changes