domCongr_support — Mathlib

English

The support of the domCongr image equals the support of f mapped by e: domCongr k A e f).support = f.support.map e.

Русский

Поддержка образа domCongr равна образу поддержки f через e: domCongr k A e f).support = f.support.map e.

LaTeX

$$$\\mathrm{domCongr}\\ k\\;A\\;e\\;f\\,\\mathrm{support} = \\mathrm{f\\,support}.map\\ e$$$

Lean4

@[to_additive (attr := simp)]
theorem domCongr_support (e : G ≃* H) (f : MonoidAlgebra A G) : (domCongr k A e f).support = f.support.map e :=
  rfl

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