Theorem Tactic.Abel.subst_into_smul_upcast

Modification history