Commit 2023-03-12 21:48 c24d3293

View on Github →

feat: port Algebra.Star.Subalgebra (#2819) Note: Lean was continually crashing on me as I was porting this file, I believe sure to autoparams.

Estimated changes

added theorem StarAlgHom.ext_adjoin
added theorem StarAlgHom.map_adjoin
added theorem StarSubalgebra.coe_bot
added theorem StarSubalgebra.coe_inf
added theorem StarSubalgebra.coe_map
added theorem StarSubalgebra.coe_top
added theorem StarSubalgebra.copy_eq
added theorem StarSubalgebra.ext
added theorem StarSubalgebra.map_id
added theorem StarSubalgebra.map_map
added theorem StarSubalgebra.map_sup
added theorem StarSubalgebra.mem_bot
added theorem StarSubalgebra.mem_inf
added theorem StarSubalgebra.mem_map
added theorem StarSubalgebra.mem_top
added structure StarSubalgebra
added theorem Subalgebra.coe_star
added theorem Subalgebra.star_mono