restrictScalarsId'App_inv_apply — Mathlib

English

The naturality square for restrictScalarsId'App with a morphism φ is satisfied: restrictScalars f .map φ ; restrictScalarsId'App N = restrictScalarsId'App M ; restrictScalars f .map φ.

Русский

Натуральность композиции для restrictScalarsId'App и отображения φ выполняется: restrictScalars f .map φ ; restrictScalarsId'App N = restrictScalarsId'App M ; restrictScalars f .map φ.

LaTeX

$$$ (\restrictScalars f).map(\varphi) \; \gg \; (\restrictScalarsId'App f hf N).hom = (\restrictScalarsId'App f hf M).hom \; \gg \; \varphi. $$$$

Lean4

@[simp]
theorem restrictScalarsId'App_inv_apply (M : ModuleCat R) (x : M) : (restrictScalarsId'App f hf M).inv x = x :=
  rfl

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