coe_ofEq_apply — Mathlib

English

The inverse of the equality-based linear equivalence corresponding to p = q equals the equivalence with swapped roles.

Русский

Обратное к эквивалентности, соответствующей p = q, есть та же эквивалентность с перестановкой модулей.

LaTeX

$$ofEq_symm (h : p = q) : (ofEq p q h).symm = ofEq q p h.symm$$

Lean4

@[simp]
theorem coe_ofEq_apply (h : p = q) (x : p) : (ofEq p q h x : M) = x :=
  rfl

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