norm_comm — Mathlib

English

Morphism norm commutes with the representation morphisms: for any f, f ≫ norm B = norm A ≫ f.

Русский

Гомоморфизм нормы коммутирует с морфизмами представления: для любого f выполняется f ∘ norm B = norm A ∘ f.

LaTeX

$$$$ f \\;\\circ\\; B.norm = A.norm \\circ f. $$$$

Lean4

@[reassoc, elementwise]
theorem norm_comm {A B : Rep k G} (f : A ⟶ B) : f ≫ norm B = norm A ≫ f :=
  by
  ext
  simp [Representation.norm, hom_comm_apply]

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