mathlib

1bef0e2c - feat(algebra/star/subalgebra): operations on `star_subalgebra`s (#17136)

feat(algebra/star/subalgebra): operations on `star_subalgebra`s (#17136) This adds more API for `star_subalgebra`s. In this PR we provide: * `star_subalgebra.inclusion : S₁ →⋆ₐ[R] S₂` when `S₁ ≤ S₂` are `star_subalgebra`s. * an instance of `has_involutive_star` for `subalgebra R A` given by applying `star` pointwise when the hypotheses on `R` and `A` include enough `star` properties. * a constructor `star_subalgebra.adjoin` which creates the minimal `star_subalgebra` containing a given `s : set A`. * a complete lattice structure on `star_subalgebra` created from the natural Galois insertion associated to `star_subalgebra.adjoin`. * some basic API for working with `star_subalgebra.adjoin` including `star_subalgebra.adjoin_induction` and variants, along with `star_alg_hom.ext_adjoin`.