Theorems · Theorem · nonassociative algebras

LieSubmodule.iSup_induction

∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {motive : M → Prop}
  {x : M},
  x ∈ ⨆ i, N i →
    (∀ (i : ι), ∀ y ∈ N i, motive y) → motive 0 → (∀ (y z : M), motive y → motive z → motive (y + z)) → motive x

Defined in

Mathlib.Algebra.Lie.Submodule

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingLieRingAddCommGroupModuleLieRingModule