English
Composition of root-pairing equivalences is associative: comp (comp h g) f = comp h (comp g f).
Русский
Композиция эквивалентностей корневой пары удовлетворяет ассоциативности: comp (comp h g) f = comp h (comp g f).
LaTeX
$$$ (comp \\; (comp\, h\, g))\, f = (comp\\; h)\\; (comp\\; g\\; f) $$$
Lean4
@[simp]
theorem comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁]
[AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃]
[Module R N₃] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂}
{P₃ : RootPairing ι₃ R M₃ N₃} (h : RootPairing.Equiv P₂ P₃) (g : RootPairing.Equiv P₁ P₂)
(f : RootPairing.Equiv P P₁) : comp (comp h g) f = comp h (comp g f) := by ext <;> simp
