coweightEquiv_comp_toLin — Mathlib

English

The map toHom of the identity equivalence is the identity homomorphism.

Русский

Образ toHom тождественного эквивалентности есть гомоморфизм-идентификатор.

LaTeX

$$$ (1 : RootPairing.Equiv P P).toHom = 1 $$$

Lean4

@[simp]
theorem coweightEquiv_comp_toLin {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
    coweightEquiv P P (Equiv.comp x y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y := by ext; simp

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