Theorems · Theorem · nonassociative algebras

NonUnitalNonAssocSemiring.mem_center_iff

∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (a : α),
  a ∈ NonUnitalSubsemiring.center α ↔
    AddMonoid.End.mulRight a = AddMonoid.End.mulLeft a ∧ AddMonoid.End.mulLeft a ∈ (CentroidHom.toEndRingHom α).rangeS

Defined in

Mathlib.Algebra.Ring.CentroidHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiring