Commit 2021-10-28 17:00 22d32dcd
View on Github →fix(field_theory/intermediate_field): use a better algebra.smul definition, and generalize (#10012)
Previously coe_smul was not true by rfl
fix(field_theory/intermediate_field): use a better algebra.smul definition, and generalize (#10012)
Previously coe_smul was not true by rfl