valueRingHom — Mathlib

English

The map Germ(𝓝 x) E →+* E is a ring homomorphism, by combining valueMulHom and valueAddHom.

Русский

Отображение жерма в колец E является гомоморфизмом колец, полученным из valueMulHom и valueAddHom.

LaTeX

$$def valueRingHom {X E : Type*} [Semiring E] [TopologicalSpace X] {x : X} : Germ (𝓝 x) E →+* E$$

Lean4

/-- The map `Germ (𝓝 x) E → E` as a ring homomorphism -/
def valueRingHom {X E : Type*} [Semiring E] [TopologicalSpace X] {x : X} : Germ (𝓝 x) E →+* E :=
  { Filter.Germ.valueMulHom, Filter.Germ.valueAddHom with }

Похожие утверждения