equivOfEq_symm — Mathlib

English

If S and T are related by equality, the corresponding algebra equivalence is symmetric: (equivOfEq S T h).symm = equivOfEq T S h.symm.

Русский

Если S и T связаны равенством, соответствующее алгебраическое эквивленое отображение симметрично: (equivOfEq S T h).symm = equivOfEq T S h.symm.

LaTeX

$$$\bigl(\text{equivOfEq } S T h\bigr)^{\!\!\,\!}\mathrm{symm} = \text{equivOfEq } T S h^{\mathrm{symm}}$$$

Lean4

@[simp]
theorem equivOfEq_symm (S T : Subalgebra R A) (h : S = T) : (equivOfEq S T h).symm = equivOfEq T S h.symm :=
  rfl

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