instMonoid

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.instMonoid

English

The map toGerm is a monoid homomorphism from AEEqFun to the germs of α-valued γ.

Русский

Отображение toGerm является гомоморфизмом моноидов от AEEqFun к Germ γ.

LaTeX

$$$\text{toGermMonoidHom} : (α \to_{μ} γ) \to_* (ae μ).Germ γ$$$

Lean4

@[to_additive existing]
instance instMonoid : Monoid (α →ₘ[μ] γ) :=
  toGerm_injective.monoid toGerm one_toGerm mul_toGerm pow_toGerm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru