English
If A has trivial star and compatible actions, starL' provides a continuous linear equivalence A ≃L A.
Русский
При тривиальном знаке звезды и совместимых действиях starL' задаёт непрерывное линейное эквивалентное отображение A ≃ L A.
LaTeX
$$$A \xrightarrow{\sim} A$ as a continuous linear equivalence.$$
Lean4
/-- If `A` is a topological module over a commutative `R` with trivial star and compatible actions,
then `star` is a continuous linear equivalence. -/
@[simps!]
def starL' (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A]
[Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : A ≃L[R] A :=
(starL R : A ≃L⋆[R] A).trans
({ AddEquiv.refl A with
map_smul' := fun r a => by simp
continuous_toFun := continuous_id
continuous_invFun := continuous_id } :
A ≃L⋆[R] A)
