Theorems · Definition · Lie groups

ContinuousMonoidHom.toMonoidHom

{A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → (A →ₜ* B) → A →* B

Reinterpret a ContinuousMonoidHom as a MonoidHom.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

4 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MonoidMonoidTopologicalSpaceTopologicalSpace