smul_mem_smul — Mathlib

English

There is a smul_induction principle for Submodule: any property holding on I • N extends from base to all of I • N.

Русский

Существует принцип индукции по умножению для Submodule: свойство, выполняющееся на I • N, распространяется по всей I • N.

LaTeX

$$$\\text{smul_induction_on} : \\forall x\\in I\\cdot N, \\; p(x)\\text{ holds provided it holds for generators}$$$

Lean4

theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N :=
  AddSubmonoid.smul_mem_smul hr hn

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