isMulFreimanIso — Mathlib

English

If f is a bijective equivalence between A and B (in the Freiman sense), then f is an n-Freiman iso.

Русский

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

LaTeX

$$$BijOn f\\ A\\ B \\Rightarrow IsMulFreimanIso n A B f$$$

Lean4

@[to_additive]
theorem isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : BijOn f A B) : IsMulFreimanIso n A B f
    where
  bijOn := hfAB
  map_prod_eq_map_prod s t _ _ _ _ := by rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]

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