withOneCongr_trans — Mathlib

English

The with-one congruence is compatible with composition: e1.withOneCongr.trans e2.withOneCongr = (e1.trans e2).withOneCongr.

Русский

Соотношение WithOne сохраняет композицию: e1.withOneCongr.trans e2.withOneCongr = (e1.trans e2).withOneCongr.

LaTeX

$$$e_1.withOneCongr.trans e_2.withOneCongr = (e_1.trans e_2).withOneCongr$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.MulEquiv.withOneCongr_trans (e₁ : α ≃* β) (e₂ : β ≃* γ) :
    e₁.withOneCongr.trans e₂.withOneCongr = (e₁.trans e₂).withOneCongr :=
  MulEquiv.toMonoidHom_injective (mapMulHom_comp _ _).symm

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