Commit 2025-03-24 11:59 c441f7b6

View on Github →

feat: add closure_insert_one etc (#23159)

Estimated changes

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

modified theorem Algebra.adjoin_empty

added theorem Algebra.adjoin_insert_algebraMap

added theorem Algebra.adjoin_insert_intCast

added theorem Algebra.adjoin_insert_natCast

added theorem Algebra.adjoin_insert_one

added theorem Algebra.adjoin_insert_zero

added theorem Algebra.adjoin_singleton_algebraMap

added theorem Algebra.adjoin_singleton_intCast

added theorem Algebra.adjoin_singleton_natCast

added theorem Algebra.adjoin_singleton_zero

modified theorem Algebra.adjoin_univ

Modified Mathlib/Algebra/Group/Subgroup/Lattice.lean

added theorem Subgroup.closure_insert_one

Modified Mathlib/Algebra/Group/Submonoid/Basic.lean

added theorem Submonoid.closure_insert_one

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

added theorem Subring.closure_insert_intCast

added theorem Subring.closure_insert_natCast

added theorem Subring.closure_insert_one

added theorem Subring.closure_insert_zero

added theorem Subring.closure_singleton_intCast

added theorem Subring.closure_singleton_natCast

added theorem Subring.closure_singleton_one

added theorem Subring.closure_singleton_zero

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

added theorem Subsemiring.closure_insert_natCast

added theorem Subsemiring.closure_insert_one

added theorem Subsemiring.closure_insert_zero

added theorem Subsemiring.closure_singleton_natCast

added theorem Subsemiring.closure_singleton_one

added theorem Subsemiring.closure_singleton_zero