coe_restrictScalars — Mathlib

English

Reinterpreting an A-alternating map as an R-alternating map when A is an R-algebra and actions are compatible yields a natural restriction map.

Русский

Переопределение A-четной карты как R-четной карты, когда A — алгебра над R и действии согласованы, задаёт естественное отображение ограничений.

LaTeX

$$$\text{restrictScalars} : (M [⋀^ι]→L[A] N) \to (M [⋀^ι]→L[R] N).$$$

Lean4

@[simp]
theorem coe_restrictScalars (f : M [⋀^ι]→L[A] N) : ⇑(f.restrictScalars R) = f :=
  rfl

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