Theorems · Theorem · nonassociative algebras

LieSubmodule.trace_eq_trace_restrict_of_le_idealizer

∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M)
  (I : LieIdeal R L) (h : I ≤ N.idealizer) (x : L) {y : L} (hy : y ∈ I)
  (hy' : optParam (∀ m ∈ N, ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) m ∈ N) ⋯),
  (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) =
    (LinearMap.trace R ↥N) (((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y).restrict hy')

Defined in

Mathlib.Algebra.Lie.TraceForm

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleModule.FreeModule.FiniteIsDomainIsPrincipalIdealRing