mathlib3
22d32dcd - fix(field_theory/intermediate_field): use a better `algebra.smul` definition, and generalize (#10012)

Commit

4 years ago

fix(field_theory/intermediate_field): use a better `algebra.smul` definition, and generalize (#10012) Previously coe_smul was not true by `rfl`

Author

eric-wieser

Parents