isMulFreimanHom_empty — Mathlib

English

For any B and f, the Freiman homomorphism A = ∅ holds for any n; i.e., every f is an n-Freiman-hom between ∅ and B.

Русский

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

LaTeX

$$$IsMulFreimanHom n\\ (\\emptyset : Set\\ α)\\ B\\ f$$$

Lean4

@[to_additive (attr := simp)]
theorem isMulFreimanHom_empty : IsMulFreimanHom n (∅ : Set α) B f
    where
  mapsTo := mapsTo_empty f B
  map_prod_eq_map_prod s t := by aesop (add simp eq_zero_of_forall_notMem)

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