Commit 2022-02-02 10:56 a687cbfb
View on Github →feat(field_theory/intermediate_field, ring_theory/.., algebra/algebra… (#11168)
If E is an subsemiring/subring/subalgebra/intermediate_field and e is an equivalence of the larger semiring/ring/algebra/field, then e induces an equivalence from E to E.map e. We define this equivalence.