Theorem IntermediateField.coe_smul

Modification history

2025-04-09 03:56
Mathlib/FieldTheory/IntermediateField/Basic.lean
feat: generalize Mathlib.FieldTheory (#23191) …
Modified IntermediateField.coe_smulView on Github →
2023-05-23 11:55
Mathlib/FieldTheory/IntermediateField.lean
feat: port FieldTheory.IntermediateField (#4258)
Added IntermediateField.coe_smulView on Github →