zpow_toGerm

Mathlib.MeasureTheory.Function.AEEqFun

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

English

Reiterates that division respects germ passage, i.e., (f/g).toGerm = f.toGerm / g.toGerm.

Русский

Повторение того, что деление сохраняет переход к Germ: (f/g).toGerm = f.toGerm / g.toGerm.

LaTeX

$$(f / g).toGerm = f.toGerm / g.toGerm$$

Lean4

@[simp]
theorem zpow_toGerm (f : α →ₘ[μ] γ) (n : ℤ) : (f ^ n).toGerm = f.toGerm ^ n :=
  comp_toGerm _ _ _

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

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

Разделы

Аффилиация

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