English
Under base change, the slope function is compatible: slope after base-changing to B and applying f to inputs equals f of the slope over A.
Русский
При базовом изменении наклонная функция совместима: наклон после базового изменения на B и применения f к входам равен f от наклона над A.
LaTeX
$$$ (W'.baseChange K).toAffine.slope (f x_1) (f x_2) (f y_1) (f y_2) = f ((W'.baseChange F).toAffine.slope x_1 x_2 y_1 y_2) $$$
Lean4
theorem baseChange_slope [DecidableEq F] [DecidableEq K] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K]
[Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) (x₁ x₂ y₁ y₂ : F) :
(W'.baseChange K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((W'.baseChange F).toAffine.slope x₁ x₂ y₁ y₂) :=
by rw [← RingHom.coe_coe, ← map_slope, map_baseChange]