inv — Mathlib

English

If f is an n-Freiman-hom between A and B, then the inverse map on B to A is an n-Freiman-hom between B^{-1} and A^{-1}.

Русский

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

LaTeX

$$$IsMulFreimanHom n A B f \\Rightarrow IsMulFreimanHom n A B^{-1} f^{-1}$$$

Lean4

@[to_additive]
theorem inv (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A B⁻¹ f⁻¹
    where
  mapsTo := hf.mapsTo.inv
  map_prod_eq_map_prod s t hsA htA hs ht
    h := by rw [Pi.inv_def, prod_map_inv, prod_map_inv, hf.map_prod_eq_map_prod hsA htA hs ht h]

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