Theorems · Theorem · linear algebra

Module.Basis.mem_center_iff

∀ {ι : Type u_1} {R : Type u_3} {A : Type u_7} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A] (b : Module.Basis ι R A)
  {z : A},
  z ∈ Set.center A ↔
    (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)

An element of a non-unital-non-associative algebra is in the center exactly when it commutes with the basis elements.

Defined in

Mathlib.LinearAlgebra.Basis.Submodule

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringNonUnitalNonAssocSemiringModuleSMulCommClassSMulCommClassIsScalarTower