Theorems · Theorem · commutative algebra

Submodule.set_smul_inductionOn

∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] {s : Set S} {N : Submodule R M}
  {motive : (x : M) → x ∈ s • N → Prop} (x : M) (hx : x ∈ s • N),
  (∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯) →
    (∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯) →
      (∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N), motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯) →
        motive 0 ⋯ → motive x hx

Induction principle for set acting on submodules. To prove P holds for all s • N, it is enough to prove: - for all r ∈ s and n ∈ N, P (r • n); - for all r and m ∈ s • N, P (r • n); - for all m₁, m₂, P m₁ and P m₂ implies P (m₁ + m₂); - P 0. To invoke this induction principle, use induction x, hx using Submodule.set_smul_inductionOn where x : M and hx : x ∈ s • N

Defined in

Mathlib.Algebra.Module.Submodule.Pointwise

Cited by

4 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleMonoidDistribMulAction