Commit 2023-03-02 18:05 c310cfdc

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.