isMulFreimanHom — Mathlib

English

If a map f is a Freiman isomorphism of order 2 between A and B, then it is also a Freiman homomorphism of order 2 from A to B.

Русский

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

LaTeX

$$IsMulFreimanIso 2 A B f → IsMulFreimanHom 2 A B f$$

Lean4

@[to_additive]
theorem isMulFreimanHom (hf : IsMulFreimanIso n A B f) : IsMulFreimanHom n A B f
    where
  mapsTo := hf.bijOn.mapsTo
  map_prod_eq_map_prod _s _t hsA htA hs ht := (hf.map_prod_eq_map_prod hsA htA hs ht).2

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