sumCongr_symm — Mathlib

English

The symmetric of sumCongr equals the sumCongr of symmetric components: (e.sumCongr f).symm = e.symm.sumCongr f.symm.

Русский

Симметрическая часть sumCongr равна sumCongr симметричных компонент: (e.sumCongr f).symm = e.symm.sumCongr f.symm.

LaTeX

$$ (Equiv.sumCongr e f).symm = Equiv.sumCongr e.symm f.symm$$

Lean4

@[simp]
theorem sumCongr_symm {α β γ δ} (e : α ≃ β) (f : γ ≃ δ) : (Equiv.sumCongr e f).symm = Equiv.sumCongr e.symm f.symm :=
  rfl

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