weightEquiv_comp_toLin — Mathlib

English

The product of weight equivalences corresponds to the composition in the opposite order: weightEquiv x y equals y followed by x.

Русский

Произведение весовых эквивалентностей соответствует композиции в обратном порядке: weightEquiv x y равен y затем x.

LaTeX

$$$ weightEquiv P P x \\; * \\; weightEquiv P P y = weightEquiv P P y \\llcorner\\; weightEquiv P P x $$$

Lean4

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

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