Commit 2024-04-03 23:28 2b6a6f13

View on Github →

chore: rename StarSubalgebra.adjoin to StarAlgebra.adjoin (#11339) This makes it consistent with all the other adjoin in the library

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

modified theorem NonUnitalStarSubalgebra.unitization_range

Modified Mathlib/Algebra/Star/Subalgebra.lean

added def StarAlgebra.adjoin

added def StarAlgebra.adjoinCommRingOfComm

added def StarAlgebra.adjoinCommSemiringOfComm

added theorem StarAlgebra.adjoin_eq_starClosure_adjoin

added theorem StarAlgebra.adjoin_induction'

added theorem StarAlgebra.adjoin_induction

added theorem StarAlgebra.adjoin_induction₂

added theorem StarAlgebra.adjoin_le

added theorem StarAlgebra.adjoin_le_iff

added theorem StarAlgebra.adjoin_toSubalgebra

added theorem StarAlgebra.self_mem_adjoin_singleton

added theorem StarAlgebra.star_self_mem_adjoin_singleton

added theorem StarAlgebra.star_subset_adjoin

added theorem StarAlgebra.subset_adjoin

deleted def StarSubalgebra.adjoin

deleted def StarSubalgebra.adjoinCommRingOfComm

deleted def StarSubalgebra.adjoinCommSemiringOfComm

deleted theorem StarSubalgebra.adjoin_eq_starClosure_adjoin

deleted theorem StarSubalgebra.adjoin_induction'

deleted theorem StarSubalgebra.adjoin_induction

deleted theorem StarSubalgebra.adjoin_induction₂

deleted theorem StarSubalgebra.adjoin_le

deleted theorem StarSubalgebra.adjoin_le_iff

deleted theorem StarSubalgebra.adjoin_toSubalgebra

deleted theorem StarSubalgebra.self_mem_adjoin_singleton

deleted theorem StarSubalgebra.star_self_mem_adjoin_singleton

deleted theorem StarSubalgebra.star_subset_adjoin

deleted theorem StarSubalgebra.subset_adjoin

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

Modified Mathlib/Topology/ContinuousFunction/Polynomial.lean

Modified test/set_like.lean