coe_restrictScalars_symm — Mathlib

English

Restriction of scalars for algebraic equivalences is compatible with composition.

Русский

Ограничение по скалярам для алгебраических эквивалентностей совместимо с композициями.

LaTeX

$$$ restrictScalars\ R\ (f \circ g) = (restrictScalars\ R\ f) \circ (restrictScalars\ R\ g)$$$

Lean4

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

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