Commit 2024-07-28 19:09 145c77aa

View on Github →

feat(Topology/Algebra/Algebra): add ContinuousAlgHom (#12800) We add the type ContinuousAlgHom for continuous algebra homomorphisms.

Estimated changes

added def AlgHom.prodMap
added theorem AlgHom.eqOn_sup
modified def AlgHom.equalizer
added theorem AlgHom.equalizer_same
added theorem AlgHom.le_equalizer
modified theorem AlgHom.mem_equalizer
added theorem AlgHom.eqOn_adjoin_iff
added theorem ContinuousAlgHom.ext
added structure ContinuousAlgHom
added theorem Subalgebra.coe_valA'
added theorem Subalgebra.coe_valA
added def Subalgebra.valA
added theorem Subalgebra.valA_apply
added theorem Submodule.range_valA