coe_restrictScalars_symm' — Mathlib

English

For an algebra equivalence f: A ≃ₛ B, the underlying function of the inverse of the restriction of scalars equals the inverse of f.

Русский

Для эквивалентности алгебр f: A ≃ₛ B, соответствие подстановки через ограничение скаляров имеет тот же обратный отображение, что и f.

LaTeX

$$$$\\big( (\\operatorname{restrictScalars}\\_R f)^{-1} \\big) = f^{-1}$$$$

Lean4

@[simp]
theorem coe_restrictScalars_symm' (f : A ≃ₐ[S] B) : ((restrictScalars R f).symm : B → A) = f.symm :=
  rfl

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