English
Dependent power induction principle (left) for Submodule powers.
Русский
Зависимый принцип индукции по степеням слева для подмодулей.
LaTeX
$$$\\text{pow\\_induction\\_on\\_left'}$$$
Lean4
/-- Dependent version of `Submodule.pow_induction_on_left`. -/
@[elab_as_elim]
protected theorem pow_induction_on_left' {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 ‹_› ‹_›))
(mem_mul : ∀ m (hm : m ∈ M), ∀ (i x hx), C i x hx → C i.succ (m * x) ((pow_succ' M i).symm ▸ (mul_mem_mul hm hx)))
{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 => mem_mul _ hm _ _ _ (n_ih ih))
(fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx
