of_fg

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

URI: https://scilib.ai/kg/mathlib#IsLinearSet.of_fg

English

If P is finitely generated, then P, viewed as a subset of M, is linear.

Русский

Если P конечно порожден, тогда P как подмножество M линейно.

LaTeX

$$$ IsLinearSet (P : Set M) $ given $ P.FG $.$$

Lean4

theorem of_fg {P : AddSubmonoid M} (hP : P.FG) : IsLinearSet (P : Set M) :=
  by
  rw [isLinearSet_iff_exists_fg_eq_vadd]
  exact ⟨0, P, hP, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru