apply_coe_symm_apply — Mathlib

English

There is a natural equivalence between MulEquiv P Q and MulEquiv Q P given by taking inverses.

Русский

Существует естественная эквивалентность между MulEquiv P Q и MulEquiv Q P, задаваемая взятием обратного.

LaTeX

$$$$\mathrm{symmEquiv} (P,Q) : (\,P \simeq^* Q\,) \simeq (Q \simeq^* P).$$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.MulEquivClass.apply_coe_symm_apply {α β} [Mul α] [Mul β] {F} [EquivLike F α β] [MulEquivClass F α β]
    (e : F) (x : β) : e ((e : α ≃* β).symm x) = x :=
  (e : α ≃* β).right_inv x

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