Theorem NonUnitalAlgebra.mem_adjoin_of_mem

Modification history

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