English
Dependent power induction principle (right) for Submodule powers.
Русский
Зависимый принцип индукции по степеням справа для подмодулей.
LaTeX
$$$\\text{pow\\_induction\\_on\\_right'}$$$
Lean4
/-- Dependent version of `Submodule.pow_induction_on_right`. -/
@[elab_as_elim]
protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop}
(algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
(add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
(mul_mem : ∀ i x hx, C i x hx → ∀ m (hm : m ∈ M), C i.succ (x * m) (mul_mem_mul hx hm)) {n : ℕ} {x : A}
(hx : x ∈ M ^ n) : C n x hx := by
induction n generalizing x with
| zero =>
rw [pow_zero] at hx
obtain ⟨r, rfl⟩ := mem_one.mp hx
exact algebraMap r
| succ n n_ih =>
revert hx
simp_rw [pow_succ]
exact fun hx ↦
Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
(fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx
