domCongr_refl — Mathlib

English

The identity equivalence on α induces the identity additive equivalence on α →₀ M.

Русский

Тождественное отображение на α порождает тождественную аддитивную эквивалентность на α →₀ M.

LaTeX

$$$\\mathrm{domCongr}(\\mathrm{refl}\\; \\alpha) = \\mathrm{AddEquiv.refl}(\\alpha →₀ M)$$$

Lean4

@[simp]
theorem domCongr_refl [AddCommMonoid M] : Finsupp.domCongr (Equiv.refl α) = AddEquiv.refl (α →₀ M) :=
  AddEquiv.ext fun _ => equivMapDomain_refl _

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