smul_induction_on

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.smul_induction_on

← MathLib Explorer

English

If I ≤ J and N ≤ P then I • N ≤ J • P.

Русский

Если I ≤ J и N ≤ P, то I • N ≤ J • P.

LaTeX

$$$I \\le J \\rightarrow N \\le P \\rightarrow I \\cdot N \\le J \\cdot P$$$

Lean4

@[elab_as_elim]
theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n))
    (add : ∀ x y, p x → p y → p (x + y)) : p x :=
  AddSubmonoid.smul_induction_on H smul add

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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