Theorem StarAlgebra.mem_adjoin_of_mem

Modification history

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