coe_symm_apply_apply — Mathlib

English

A general fact: applying an equivalence and then its inverse returns the original element.

Русский

Общее свойство: применение эквивалентности и затем её обратного возвращает исходный элемент.

LaTeX

$$$$ (e : \\alpha \\simeq^* \\beta) ((e : \\alpha \\simeq^* \\beta).symm\, x) = x. $$$$

Lean4

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

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