Theorems · Theorem · nonassociative algebras

LieRinehartSubalgebra.mk.inj

∀ {A : Type u_1} {L : Type u_2} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {toSubmodule : Submodule A L}
  {lie_mem' : ∀ {a b : L}, a ∈ toSubmodule.carrier → b ∈ toSubmodule.carrier → ⁅a, b⁆ ∈ toSubmodule.carrier}
  {toSubmodule_1 : Submodule A L}
  {lie_mem'_1 : ∀ {a b : L}, a ∈ toSubmodule_1.carrier → b ∈ toSubmodule_1.carrier → ⁅a, b⁆ ∈ toSubmodule_1.carrier},
  { toSubmodule := toSubmodule, lie_mem' := lie_mem' } = { toSubmodule := toSubmodule_1, lie_mem' := lie_mem'_1 } →
    toSubmodule = toSubmodule_1

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms