English
A simplified version of the induction principle for regular sequences in which the motive does not depend on the proof of regularity. The principle still allows deriving properties along the front-prepended step but with a simplified motive.
Русский
Упрощенная версия принципа индукции по регулярам последовательности, при которой мотива не зависит от доказательства регулярности. Принцип позволяет переносить свойства по шагам добавления элемента спереди, упрощая мотив.
LaTeX
$$$\\text{ndrecIterModByRegular}\;\\Big(\\text{nil},\\text{cons}\\Big): IsRegular(M, rs) \\to \\text{motive}(M, rs)$$$
Lean4
/-- A simplified version of `IsRegular.recIterModByRegular` where the motive is
not allowed to depend on the proof of `IsRegular`. -/
def ndrecIterModByRegular {motive : (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → Sort*}
(nil : (M : Type v) → [AddCommGroup M] → [Module R M] → [Nontrivial M] → motive M [])
(cons :
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
IsSMulRegular M r → IsRegular (QuotSMulTop r M) rs → motive (QuotSMulTop r M) rs → motive M (r :: rs))
{M} [AddCommGroup M] [Module R M] {rs} : IsRegular M rs → motive M rs :=
recIterModByRegular (motive := fun M _ _ rs _ => motive M rs) nil cons
