Theorem IntermediateField.adjoin_natCast

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.adjoin_natCast View on Github →

2024-04-07 17:47

Mathlib/FieldTheory/Adjoin.lean

chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …

Added IntermediateField.adjoin_natCast View on Github →