Theorem IntermediateField.map_comap_eq

Modification history

2025-01-10 01:57

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) …

Modified IntermediateField.map_comap_eq View on Github →

2024-07-31 06:44

Mathlib/FieldTheory/Adjoin.lean

feat: add `comap_map` for sub(semi)ring, subalgebra, subfield and intermediate fields (#15193) …

Added IntermediateField.map_comap_eq View on Github →