English
For f and h as linear maps with base-change properties, the base-change condition for the composed map is equivalent to the product of base-change conditions.
Русский
Если f и h удовлетворяют свойствам базового изменения, то базовое изменение композиции равно условию произведения базовых изменений.
LaTeX
$$$ IsBaseChange S f \to IsBaseChange T g \Leftrightarrow IsBaseChange T (g \circ f)$$$
Lean4
/-- If `N` is the base change `M` to `S`, then `O` is the base change of `M` to `T` if and
only if `O` is the base change of `N` to `T`. -/
theorem comp_iff {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N →ₗ[S] O} :
IsBaseChange T ((h : N →ₗ[R] O) ∘ₗ f) ↔ IsBaseChange T h :=
⟨fun hc ↦ IsBaseChange.of_comp hf hc, fun hh ↦ IsBaseChange.comp hf hh⟩
