toEquiv_symm — Mathlib

English

The inverse of a multiplicative equivalence, as an equivalence, corresponds to the symmetric equivalence: (f.symm) corresponds to (f).symm.

Русский

Обратный мультипликативный эквивалент, как эквив, соответствует симметричной эквивалентности: (f.symm) соответствует (f).symm.

LaTeX

$$$\\mathrm{MulEquiv}.toEquiv\\;\\mathrm{symm}(f) = (\\mathrm{MulEquiv}.toEquiv\\;f)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem toEquiv_symm (f : M ≃* N) : (f.symm : N ≃ M) = (f : M ≃ N).symm :=
  rfl

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