Theorem IntermediateField.algebraAdjoinAdjoin.coe_algebraMap

Modification history

2026-03-04 08:58
Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
feat(FieldTheory/RatFunc): Degree of field extension K(X)/K(f) (#34215) …
Added IntermediateField.algebraAdjoinAdjoin.coe_algebraMapView on Github →