English
Let C be a predicate on A. If C holds for scalars, is closed under addition, and is stable under right multiplication by elements of M, then C holds for every x ∈ M^n when x ∈ M^n.
Русский
Пусть C — свойство на A. если C выполняется для скаляров, замкнуто по сложению и устойчиво при правом умножении на элементы M, тогда C выполняется для любого x ∈ M^n, если x ∈ M^n.
LaTeX
$$$\forall C:A \to \mathsf{Prop},\; (\forall r\in R,\; C(\mathrm{algebraMap}^A_R\; r)) \\ \tto (\forall x,y,\; C(x) \to C(y) \to C(x+y)) \\ \tto (\forall x, \; C(x) \to \forall m \in M, C(x \cdot m)) \\ \tto (\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 `x * m` where `m ∈ M` and it holds for `x` -/
@[elab_as_elim]
protected theorem pow_induction_on_right {C : A → Prop} (hr : ∀ r : R, C (algebraMap _ _ r))
(hadd : ∀ x y, C x → C y → C (x + y)) (hmul : ∀ x, C x → ∀ m ∈ M, C (x * m)) {x : A} {n : ℕ} (hx : x ∈ M ^ n) :
C x :=
Submodule.pow_induction_on_right' (M := M) (C := fun _ a _ => C a) hr (fun x y _i _hx _hy => hadd x y)
(fun _i _x _hx => hmul _) hx
