Theorem Subfield.smul_def

Modification history

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