English
There is a monoid homomorphism from the germ of E at x to E given by φ ↦ φ.value.
Русский
Существет мономорфизм из жерма E в точке x в E, задаваемый φ ↦ φ.value.
LaTeX
$$def valueMulHom {X E : Type*} [Monoid E] [TopologicalSpace X] {x : X} : Germ (𝓝 x) E →* E$$
Lean4
/-- The map `Germ (𝓝 x) E → E` into a monoid `E` as a monoid homomorphism -/
@[to_additive /-- The map `Germ (𝓝 x) E → E` as an additive monoid homomorphism -/
]
def valueMulHom {X E : Type*} [Monoid E] [TopologicalSpace X] {x : X} : Germ (𝓝 x) E →* E
where
toFun := Filter.Germ.value
map_one' := rfl
map_mul' φ ψ := Germ.inductionOn φ fun _ ↦ Germ.inductionOn ψ fun _ ↦ rfl
