English
A ring-parametrized induction for IsWeaklyRegular with a motive that depends on R.
Русский
Индукция над кольцом с зависимой мотивацией IsWeaklyRegular.
LaTeX
$$$\\text{ndrecWithRing}$ expresses a ring-parametrized induction for IsWeaklyRegular.$$
Lean4
/-- A simplified version of `IsWeaklyRegular.recIterModByRegularWithRing` where
the motive is not allowed to depend on the proof of `IsWeaklyRegular`. -/
def ndrecWithRing
{motive : (R : Type u) → [CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → Sort*}
(nil : (R : Type u) → [CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → motive R M [])
(cons :
{R : Type u} →
[CommRing R] →
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
IsSMulRegular M r →
IsWeaklyRegular (QuotSMulTop r M) (rs.map (Ideal.Quotient.mk (Ideal.span { r }))) →
motive (R ⧸ Ideal.span { r }) (QuotSMulTop r M)
(rs.map (Ideal.Quotient.mk (Ideal.span { r }))) →
motive R M (r :: rs))
{R} [CommRing R] {M} [AddCommGroup M] [Module R M] {rs} : IsWeaklyRegular M rs → motive R M rs :=
recIterModByRegularWithRing (motive := fun R _ M _ _ rs _ => motive R M rs) nil cons
