domCongr_symm — Mathlib

English

For any equivalence e, the symmetric operation of domCongr corresponds to domCongr of e^{-1} between β →₀ M and α →₀ M.

Русский

Для любой эквивалентности e симметричная операция domCongr эквивалентна domCongr e^{-1} между β →₀ M и α →₀ M.

LaTeX

$$$(\\mathrm{domCongr}\; e)^{-1} = \\mathrm{domCongr}\\; e^{-1}$$$

Lean4

@[simp]
theorem domCongr_symm [AddCommMonoid M] (e : α ≃ β) :
    (Finsupp.domCongr e).symm = (Finsupp.domCongr e.symm : (β →₀ M) ≃+ (α →₀ M)) :=
  AddEquiv.ext fun _ => rfl

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