restrictScalars_toLinearMap_apply_apply

English

Applying algebra maps after restriction agrees with the original linear map evaluation.

Русский

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

LaTeX

$$$ algebraMap\ K L ( (P.restrictScalars' K hP).toLinearMap x y ) = P.toLinearMap x y $$$

Lean4

@[simp]
theorem restrictScalars_toLinearMap_apply_apply (x : span K (range P.root)) (y : span K (range P.coroot)) :
    algebraMap K L ((P.restrictScalars' K hP).toLinearMap x y) = P.toLinearMap x y := by simp [restrictScalars']

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