English
Left composition by a continuous ring homomorphism g: β →+* γ induces a RingHom from C(α, β) to C(α, γ), compatible with addition and multiplication.
Русский
Слева композиция по непрерывному кольцевому гомоморфизму g: β →+* γ индуцирует RingHom от C(α, β) к C(α, γ), совместимый по сложению и умножению.
LaTeX
$$$ RingHom\, (C(\alpha, \beta), C(\alpha, \gamma)) \text{ via left composition by } g. $$$
Lean4
/-- Composition on the left by a (continuous) homomorphism of topological semirings, as a
`RingHom`. Similar to `RingHom.compLeft`. -/
@[simps!]
protected def _root_.RingHom.compLeftContinuous (α : Type*) {β : Type*} {γ : Type*} [TopologicalSpace α]
[TopologicalSpace β] [Semiring β] [IsTopologicalSemiring β] [TopologicalSpace γ] [Semiring γ]
[IsTopologicalSemiring γ] (g : β →+* γ) (hg : Continuous g) : C(α, β) →+* C(α, γ) :=
{ g.toMonoidHom.compLeftContinuous α hg, g.toAddMonoidHom.compLeftContinuous α hg with }
