English
Let C be a predicate on A. If C holds for every algebraic image of R, is closed under addition, and is stable under left multiplication by elements of M, then C holds for every element of M^n whenever the element lies in M^n.
Русский
Пусть C — свойство на A. если C выполняется для всех образов от R через алгебраическую гомоморфию, замкнуто по сложению и устойчиво при левом умножении на элементы M, тогда C выполняется для любого элемента M^n, принадлежащего M^n.
LaTeX
$$$\forall C:A \to \mathsf{Prop},\; (\forall r\in R,\; C(\mathrm{algebraMap}^A_R\; r)) \\ to (\forall x,y,\; C(x) \to C(y) \to C(x+y)) \\ to (\forall m\in M, \forall x,\; C(x) \to C(m \cdot x)) \\ to (\forall x\in M^n,\; C(x)).$$$
Lean4
/-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
is closed under addition, and holds for `m * x` where `m ∈ M` and it holds for `x` -/
@[elab_as_elim]
protected theorem pow_induction_on_left {C : A → Prop} (hr : ∀ r : R, C (algebraMap _ _ r))
(hadd : ∀ x y, C x → C y → C (x + y)) (hmul : ∀ m ∈ M, ∀ (x), C x → C (m * x)) {x : A} {n : ℕ} (hx : x ∈ M ^ n) :
C x :=
Submodule.pow_induction_on_left' M (C := fun _ a _ => C a) hr (fun x y _i _hx _hy => hadd x y)
(fun _m hm _i _x _hx => hmul _ hm _) hx
