Theorem NonUnitalStarAlgebra.mem_adjoin_of_mem

Modification history

2025-06-23 07:20
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
chore(Algebra): replace messy `simps!` with Aesop lemmas, add a test (#26127) …
Added NonUnitalStarAlgebra.mem_adjoin_of_memView on Github →