Strengthen additive_effective_congruences_imply_normal#185

Merged

ScriptRaccoon merged 1 commit into

ScriptRaccoon:mainfrom

dschepler:strengthen-additive_effective_congruences_imply_normal

May 16, 2026

Commits on May 15, 2026

The pullback assumption for this implication turns out not to be necessary, and allows us to drop an explicit assignment in FreeAb
dschepler
committed