trans_toAlgEquiv — Mathlib

English

The underlying algebra equivalence of the composite is the composite of the underlying algebra equivalences: (e1.trans e2).toAlgEquiv = e1.toAlgEquiv.trans e2.toAlgEquiv.

Русский

Удвоенная эквивалентность сохраняется на уровне алгебраических эквивалентностей: (e1.trans e2).toAlgEquiv = e1.toAlgEquiv.trans e2.toAlgEquiv.

LaTeX

$$$(e_1 \mathrm{trans} e_2).toAlgEquiv = e_1.toAlgEquiv.trans e_2.toAlgEquiv$$$

Lean4

@[simp]
theorem trans_toAlgEquiv (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :
    (e₁.trans e₂).toAlgEquiv = e₁.toAlgEquiv.trans e₂.toAlgEquiv :=
  rfl

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