Def IntermediateField.RingHom.adjoinAlgebraMap

Modification history

2026-01-22 10:30
Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
feat: RingHom.adjoinAlgebraMap (#33016) …
Added IntermediateField.RingHom.adjoinAlgebraMapView on Github →