Theorems · Theorem · nonassociative algebras

LieRinehartSubalgebra.mem_mk_iff

∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L] (S : Set L)
  (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0)
  (h₃ :
    ∀ (c : A) {x : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {a b : L},
      a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
          ⁅a, b⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier)
  {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } ↔ x ∈ S

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

CommRingLieRingModule