freeGroupCongr_symm — Mathlib

English

The inverse of the congruence for e is the congruence for e.symm: (freeGroupCongr e).symm = freeGroupCongr e.symm.

Русский

Обратное к эквивалентности соответствие — эквивалентность для обратной эквивалентности: (freeGroupCongr e).symm = freeGroupCongr e.symm.

LaTeX

$$$ (freeGroupCongr\\ e).symm = freeGroupCongr\\ e.symm $$$

Lean4

@[to_additive (attr := simp)]
theorem freeGroupCongr_symm {α β} (e : α ≃ β) : (freeGroupCongr e).symm = freeGroupCongr e.symm :=
  rfl

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