English
For any NonUnitalSubalgebra S, x ∈ star S if and only if star x ∈ S.
Русский
Для любого NonUnitalSubalgebra S верно: x принадлежит star S тогда и только тогда, когда star x принадлежит S.
LaTeX
$$$x \in \operatorname{star} S \iff x^{\star} \in S$$$
Lean4
/-- The pointwise `star` of a non-unital subalgebra is a non-unital subalgebra. -/
instance instInvolutiveStar : InvolutiveStar (NonUnitalSubalgebra R A)
where
star
S :=
{ carrier := star S.carrier
mul_mem' :=
@fun x y hx hy => by
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier] using (star_mul x y).symm ▸ mul_mem hy hx
add_mem' :=
@fun x y hx hy => by
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier] using (star_add x y).symm ▸ add_mem hx hy
zero_mem' := Set.mem_star.mp ((star_zero A).symm ▸ zero_mem S : star (0 : A) ∈ S)
smul_mem' := fun r x hx => by
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier] using
(star_smul r x).symm ▸ SMulMemClass.smul_mem (star r) hx }
star_involutive
S :=
NonUnitalSubalgebra.ext fun x =>
⟨fun hx => star_star x ▸ hx, fun hx => ((star_star x).symm ▸ hx : star (star x) ∈ S)⟩
