mapDomain_mul — Mathlib

English

If f and g respect multiplication, mapDomain preserves products: mapDomain f (x*y) = mapDomain f x * mapDomain f y.

Русский

Если f и g сохраняют умножение, mapDomain сохраняет произведения.

LaTeX

$$$ mapDomain f (x \cdot y) = mapDomain f x \cdot mapDomain f y $$$

Lean4

@[to_additive (dont_translate := R) mapDomain_mul]
theorem mapDomain_mul [Mul M] [Mul N] {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F)
    (x y : MonoidAlgebra R M) : mapDomain f (x * y) = mapDomain f x * mapDomain f y := by
  simp [mul_def, mapDomain_sum, add_mul, mul_add, sum_mapDomain_index]

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