English
Freiman-homomorphisms are closed under quotients: if h1: A→B1 with f1 and h2: A→B2 with f2, then h1/h2 is a Freiman-hom between B1/B2 with f1/f2.
Русский
Фримановы гомоморфизмы замкнуты по отношению деления: если h1: A→B1 с f1 и h2: A→B2 с f2, то h1/h2 является Фримановой гомоморфией между B1/B2 и f1/f2.
LaTeX
$$$IsMulFreimanHom n A B1 f1 \\to IsMulFreimanHom n A B2 f2 \\to IsMulFreimanHom n A (B1 / B2) (f1 / f2)$$$
Lean4
@[to_additive]
theorem div {β : Type*} [DivisionCommMonoid β] {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : IsMulFreimanHom n A B₁ f₁)
(h₂ : IsMulFreimanHom n A B₂ f₂) : IsMulFreimanHom n A (B₁ / B₂) (f₁ / f₂)
where
mapsTo := h₁.mapsTo.div h₂.mapsTo
map_prod_eq_map_prod s t hsA htA hs ht
h := by
rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
h₂.map_prod_eq_map_prod hsA htA hs ht h]
