Theorem IntermediateField.smul_def

Modification history

2024-10-28 06:12
Mathlib/FieldTheory/IntermediateField/Basic.lean
feat(FieldTheory): define induced action of subfields and intermediate fields (#18141) …
Added IntermediateField.smul_defView on Github →