English
Characterisation of 2-Freiman isomorphisms: IsMulFreimanIso 2 A B f is equivalent to BijOn f A B together with the product condition for all a,b,c,d ∈ A.
Русский
Характеризация 2–Freiman изоморфизмов: IsMulFreimanIso 2 A B f эквивалентен BijOn f A B вместе с условием про произведения для всех a,b,c,d ∈ A.
LaTeX
$$IsMulFreimanIso 2 A B f ↔ BijOn f A B ∧ ∀ a∈A, ∀ b∈A, ∀ c∈A, ∀ d∈A, f a f b = f c f d ↔ a b = c d$$
Lean4
/-- Characterisation of `2`-Freiman homomorphisms. -/
@[to_additive /-- Characterisation of `2`-Freiman homomorphisms. -/
]
theorem isMulFreimanHom_two :
IsMulFreimanHom 2 A B f ↔ MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d
where
mp hf := ⟨hf.mapsTo, fun _ ha _ hb _ hc _ hd ↦ hf.mul_eq_mul ha hb hc hd⟩
mpr hf := ⟨hf.1, by aesop (add simp card_eq_two)⟩
