Commit 2023-05-18 23:40 aa666983

View on Github →

feat(topology/algebra/module/star): continuity results for star_modules (#19037) Notably this adds starL. This also fixes some unnecessary typeclass arguments in star_linear_equiv.

Estimated changes

Modified src/algebra/star/module.lean

Modified src/analysis/normed_space/star/basic.lean

added theorem starₗᵢ_to_continuous_linear_equiv

Created src/topology/algebra/module/star.lean

added theorem continuous_decompose_prod_adjoint

added theorem continuous_decompose_prod_adjoint_symm

added theorem continuous_self_adjoint_part

added theorem continuous_skew_adjoint_part

added def self_adjoint_partL

added def skew_adjoint_partL

added def starL

added def star_module.decompose_prod_adjointL