algEquiv_symm_apply — Mathlib

English

The underlying map of the inverse of algEquiv R e is e.symm.

Русский

Обратное отображение algEquiv R e имеет базовую карту e.symm.

LaTeX

$$$\\\\big(\\\\mathrm{AlgEquiv}\\\\_R(\\\\mathrm{Equiv}\\\\,e)\\\\text{).symm}\\\\ b = e^{-1}(b).$$$

Lean4

theorem algEquiv_symm_apply (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) :
    by
    letI := Equiv.semiring e
    letI := Equiv.algebra R e
    exact (algEquiv R e).symm b = e.symm b :=
  rfl

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