domLCongr_single — Mathlib

English

A domain-congruence map sends a singleton to the singleton at the image index with the same value.

Русский

Согласование домена отправляет единичный элемент в единичный по изображению индекса с тем же значением.

LaTeX

$$$(\mathrm{domLCongr}\,e)\big(\mathrm{single}\,i\,m\big) = \mathrm{single}\,(e(i))\,m$$$

Lean4

theorem domLCongr_single {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (i : α₁) (m : M) :
    (Finsupp.domLCongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by simp

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