coe_toAlgEquiv — Mathlib

English

For any continuous A ≃A[R] B, the underlying function of its AlgEquiv is exactly the same as the equivalence.

Русский

Для любой непрерывной эквивалентности A ≃A[R] B соответствующая AlgEquiv имеет ту же действующую функцию, что и сама эквивалентность.

LaTeX

$$$ (e.toAlgEquiv) = e $$$

Lean4

@[simp]
theorem coe_toAlgEquiv (e : A ≃A[R] B) : ⇑e.toAlgEquiv = e :=
  rfl

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