English
A simplified induction principle for weakly regular sequences with motive independent of the proof of IsWeaklyRegular.
Русский
Упрощённый принцип индукции для слабых регулярных последовательностей с мотивацией, независимой от доказательства IsWeaklyRegular.
LaTeX
$$$\\text{ndrecIterModByRegular}$ grants a motive-parameterized recursion for IsWeaklyRegular.$$
Lean4
/-- A simplified version of `IsWeaklyRegular.recIterModByRegular` where the
motive is not allowed to depend on the proof of `IsWeaklyRegular`. -/
def ndrecIterModByRegular {motive : (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → Sort*}
(nil : (M : Type v) → [AddCommGroup M] → [Module R M] → motive M [])
(cons :
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
IsSMulRegular M r →
IsWeaklyRegular (QuotSMulTop r M) rs → motive (QuotSMulTop r M) rs → motive M (r :: rs))
{M} [AddCommGroup M] [Module R M] {rs} : IsWeaklyRegular M rs → motive M rs :=
recIterModByRegular (motive := fun M _ _ rs _ => motive M rs) nil cons
