mathlib3

c310cfdc - chore(algebra/algebra/restrict_scalars): replace `restrict_scalars_smul_def` with version that does not commit defeq-abuse. (#18540)

chore(algebra/algebra/restrict_scalars): replace `restrict_scalars_smul_def` with version that does not commit defeq-abuse. (#18540) This lemma abuses definitional equality and I think we are better without it. My immediate motivation is the trouble it is causing in the Mathlib4 porting PR: https://github.com/leanprover-community/mathlib4/pull/2563 Note that it was only used in one place and there is a better proof.