weightEquiv_apply — Mathlib

English

For an equivalence e: P ≃ Q, weightEquiv P Q e applied to m equals e.toHom.weightMap m.

Русский

Для эквивалентности e: P ≃ Q, весовое отображение применённое к m равно весовому отображению e.toHom.weightMap на m.

LaTeX

$$weightEquiv P Q e m = e.toHom.weightMap m$$

Lean4

@[simp]
theorem weightEquiv_apply (e : RootPairing.Equiv P Q) (m : M) : weightEquiv P Q e m = e.toHom.weightMap m :=
  rfl

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