equivOfEq_trans — Mathlib

English

If we take the reflexive equality, equivOfEq rfl is the identity (refl) isomorphism.

Русский

Если взять равенство по умолчанию, equivOfEq rfl есть тождественный изоморфизм.

LaTeX

$$$\\text{equivOfEq }(\\mathrm{rfl}) = \\mathrm{AlgEquiv.refl}$$$

Lean4

@[simp]
theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
    (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
  rfl

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