English
A principled induction for weakly regular sequences: the empty sequence is weakly regular; if r is regular on M and rs is weakly regular on M/ rM, then r :: rs is weakly regular on M.
Русский
Классическая индукция по слабой регулярности: пустая последовательность слаб reg; если r регулярна на M и rs слабая регуляторная на M/ rM, тогда r :: rs слабая регуляторная на M.
LaTeX
$$$\\text{recIterModByRegular}$ defines an induction principle: (nil) and (cons) cover all IsWeaklyRegular sequences.$$
Lean4
/-- Weakly regular sequences can be inductively characterized by:
* The empty sequence is weakly regular on any module.
* If `r` is regular on `M` and `rs` is a weakly regular sequence on `M⧸rM` then
the sequence obtained from `rs` by prepending `r` is weakly regular on `M`.
This is the induction principle produced by the inductive definition above.
The motive will usually be valued in `Prop`, but `Sort*` works too. -/
@[induction_eliminator]
def recIterModByRegular
{motive : (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → IsWeaklyRegular M rs → Sort*}
(nil : (M : Type v) → [AddCommGroup M] → [Module R M] → motive M [] (nil R M))
(cons :
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
(h1 : IsSMulRegular M r) →
(h2 : IsWeaklyRegular (QuotSMulTop r M) rs) →
(ih : motive (QuotSMulTop r M) rs h2) → motive M (r :: rs) (cons h1 h2)) :
{M : Type v} → [AddCommGroup M] → [Module R M] → {rs : List R} → (h : IsWeaklyRegular M rs) → motive M rs h
| M, _, _, [], _ => nil M
| M, _, _, r :: rs, h =>
let ⟨h1, h2⟩ := (isWeaklyRegular_cons_iff M r rs).mp h
cons r rs h1 h2 (recIterModByRegular nil cons h2)
