mul_apply

Mathlib.RingTheory.AdicCompletion.Algebra

URI: https://scilib.ai/kg/mathlib#AdicCompletion.mul_apply

English

Multiplication in the AdicCauchySequence is pointwise: (f * g) n = f n * g n.

Русский

Умножение в AdicCauchySequence — покомпонентно: (f * g) n = f n · g n.

LaTeX

$$mul_apply(I,n,f,g) : (f * g) n = f n * g n$$

Lean4

@[simp]
theorem mul_apply (n : ℕ) (f g : AdicCauchySequence I R) : (f * g) n = f n * g n :=
  rfl

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

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

Разделы

Аффилиация

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