domCongr_single — Mathlib

English

For e ∈ G ≃* H, g ∈ G, a ∈ A, domCongr k A e (single g a) = single (e g) a.

Русский

Для e ∈ G ≃* H, g ∈ G, a ∈ A: domCongr k A e (single g a) = single (e g) a.

LaTeX

$$$\\mathrm{domCongr}\\ k\\;A\\;e\\;\\big(\\mathrm{single}\\ g\\ a\\big) = \\mathrm{single}\\ (e(g))\\ a$$$

Lean4

@[to_additive (attr := simp)]
theorem domCongr_single (e : G ≃* H) (g : G) (a : A) : domCongr k A e (single g a) = single (e g) a :=
  Finsupp.equivMapDomain_single _ _ _

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