English
Dependent version of smul_induction_on: a property p holds on x ∈ I • N if it holds on generators and is closed under addition.
Русский
Зависимая версия smul_induction_on: свойство p верно на x ∈ I • N, если оно верно на порождающих и замыкается по сумме.
LaTeX
$$$\\text{smul_induction_on}' : \\forall x, x\\in I\\cdot N \\Rightarrow (\\text{p holds for generators and sums})$$$
Lean4
/-- Dependent version of `Submodule.smul_induction_on`. -/
@[elab_as_elim]
theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop}
(smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn))
(add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx :=
by
refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩
