refactor: Turn Freiman homs into predicates (#12546)

The bundled hom approach to Freiman homomorphisms is a fail. It is very hard to use and doesn't bring anything. That is because Freiman homs don't have much structure and we do not study them under this angle.

This PR replaces the bundled homs by predicates and moves the file from `Algebra.Group.Freiman` to `Combinatorics.Additive.FreimanHom` so that:
* It is clear these are combinatorial objects, not algebraic ones.
* The diff isn't completely mangled. Nothing was kept so it's not worth comparing via a naïve git diff.

Also fix a few oddities accidentally introduced in #12701.

Author: YaelDillies

Mathlib.lean

@@ -200,7 +200,6 @@ import Mathlib.Algebra.Group.Embedding
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Equiv.TypeTags
 import Mathlib.Algebra.Group.Ext
-import Mathlib.Algebra.Group.Freiman
 import Mathlib.Algebra.Group.Hom.Basic
 import Mathlib.Algebra.Group.Hom.CompTypeclasses
 import Mathlib.Algebra.Group.Hom.Defs
@@ -1602,6 +1601,7 @@ import Mathlib.Combinatorics.Additive.AP.Three.Behrend
 import Mathlib.Combinatorics.Additive.AP.Three.Defs
 import Mathlib.Combinatorics.Additive.ETransform
 import Mathlib.Combinatorics.Additive.Energy
+import Mathlib.Combinatorics.Additive.FreimanHom
 import Mathlib.Combinatorics.Additive.PluenneckeRuzsa
 import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.Combinatorics.Colex