of_flat — Mathlib

English

If rs is a weakly regular R-sequence and every r in rs lies in p (prime), then the image sequence in S is regular.

Русский

Если rs — слабая регулярная последовательность по R и каждый r ∈ rs лежит в p, тогда образ этой последовательности в S является регулярной.

LaTeX

$$$\text{IsRegular}_S( rs.map(\operatorname{algebraMap}_R^S) ) \text{ under }(rs\subset p).$$$

Lean4

theorem of_flat [Flat R S] {rs : List R} (reg : IsWeaklyRegular R rs) : IsWeaklyRegular S (rs.map (algebraMap R S)) :=
  reg.of_flat_of_isBaseChange (IsBaseChange.linearMap R S)

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