of_flat — Mathlib

English

If the base change map is flat and reg is IsSMulRegular on M, then its base-changed counterpart on N is IsSMulRegular.

Русский

Если отображение базового изменения плоское и reg — IsSMulRegular на M, то его базовое изменение на N также IsSMulRegular.

LaTeX

$$$\\text{IsBaseChange } S f \\Rightarrow \\text{IsSMulRegular } M x \\Rightarrow \\text{IsSMulRegular } N (\\text{algebraMap } R S x)$$$

Lean4

theorem of_flat {x : R} (reg : IsSMulRegular R x) : IsSMulRegular S (algebraMap R S x) :=
  reg.of_flat_of_isBaseChange (IsBaseChange.linearMap R S)

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