Theorem Algebra.mem_adjoin_of_mem

Modification history

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