isMulFreimanHom — Mathlib

English

If f is a monoid homomorphism and maps A into B, then f is an n-Freiman-hom between A and B.

Русский

Если f является гомоморфизмом моноида и отображает A в B, то f является n‑Фримановой гомоморфией между A и B.

LaTeX

$$$\\MapsTo f\\ A\\ B \\Rightarrow IsMulFreimanHom n A B f$$$

Lean4

@[to_additive]
theorem isMulFreimanHom [FunLike F α β] [MonoidHomClass F α β] (f : F) (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f
    where
  mapsTo := hfAB
  map_prod_eq_map_prod s t _ _ _ _ h := by rw [← map_multiset_prod, h, map_multiset_prod]

Похожие утверждения