freeGroupCongr_trans — Mathlib

English

Composition of congruences corresponds to the congruence of the composed equivalence: (freeGroupCongr e).trans (freeGroupCongr f) = freeGroupCongr (e.trans f).

Русский

Сведение в состав конгруэнций соответствует конгруэнции отражения составленного эквивалента: (freeGroupCongr e).trans (freeGroupCongr f) = freeGroupCongr (e.trans f).

LaTeX

$$$ (freeGroupCongr\\ e).trans (freeGroupCongr\\ f) = freeGroupCongr\\ (e.trans\\ f) $$$

Lean4

@[to_additive]
theorem freeGroupCongr_trans {α β γ} (e : α ≃ β) (f : β ≃ γ) :
    (freeGroupCongr e).trans (freeGroupCongr f) = freeGroupCongr (e.trans f) :=
  MulEquiv.ext <| map.comp _ _

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