Commit 2025-06-18 18:48 bea1cb40

View on Github →

chore(Algebra/Algebra): add missing lemmas to API for some closures (#26024)

Bring the API for some adjoin and closure operators into line with the API for subalgebras in Algebra.Algebra.Subalgebra.Lattice
Add a missing gcongr tag
Moves (incidental): NonUnitalSubalgebra.starClosure_toNonunitalSubalgebra -> NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra Split from #25961, in preparation for improvement of the automation in these files

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

added theorem NonUnitalAlgebra.adjoin_mono

Modified Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

added theorem NonUnitalStarAlgebra.adjoin_mono

added theorem NonUnitalSubalgebra.coe_starClosure

added theorem NonUnitalSubalgebra.mem_starClosure

added theorem NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra

deleted theorem NonUnitalSubalgebra.starClosure_toNonunitalSubalgebra

Modified Mathlib/Algebra/Star/Subalgebra.lean

added theorem StarAlgebra.adjoin_mono

added theorem Subalgebra.coe_starClosure

added theorem Subalgebra.mem_starClosure

modified theorem Subalgebra.starClosure_toSubalgebra