English
A pointwise smul induction principle: given a submodule N and a set a of scalars, if a predicate P holds for a smul on generators, is closed under scalar smul and addition, then P holds for all elements in a • N.
Русский
Принцип индукции по точечному умножению: пусть есть подмодуль N и множество скаляр a. Если P сохраняется под умножением на элементы a на генераторах и замкну под скалярным умножением и сложением, то P выполняется для всех элементов a • N.
LaTeX
$$$\forall x\in a\cdot N\; P(x)\ \text{задаётся условий:}$ \\ (1) \forall s\in N\,\ P(a\cdot s), \quad (2) \forall r\in R, m\in a\cdot N,\ P(m)\Rightarrow P(r\cdot m), \\ (3) \forall x,y\in a\cdot N,\ P(x)\land P(y)\Rightarrow P(x+y), \\ (4) P(0) \Rightarrow \forall x\in a\cdot N, P(x).$$
Lean4
theorem smul_inductionOn_pointwise [SMulCommClass S R M] {a : S} {p : (x : M) → x ∈ a • N → Prop}
(smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) (Submodule.smul_mem_pointwise_smul _ _ _ hs))
(smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) (Submodule.smul_mem _ _ mem))
(add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) (Submodule.add_mem _ hx hy))
(zero : p 0 (Submodule.zero_mem _)) {x : M} (hx : x ∈ a • N) : p x hx :=
by
simp_all only [← Submodule.singleton_set_smul]
let p' (x : M) (hx : x ∈ ({ a } : Set S) • N) : Prop := p x (by rwa [← Submodule.singleton_set_smul])
refine
Submodule.set_smul_inductionOn (motive := p') _ (N.singleton_set_smul a ▸ hx) (fun r n hr hn ↦ ?_) smul₁ add zero
· simp only [Set.mem_singleton_iff] at hr
subst hr
exact smul₀ n hn
