inl_pow — Mathlib

English

For any list of elements in tsze.R M, the fst-coordinate of their product equals the product of their fst-coordinates.

Русский

Для любого списка элементов из tsze.R M первая координата их произведения равна произведению их первых координат.

LaTeX

$$$\\\\mathrm{fst}(\\\\prod l) = \\\\prod (\\\\mathrm{fst} \\\\circ l)$$$

Lean4

@[simp]
theorem inl_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (n : ℕ) :
    (inl r ^ n : tsze R M) = inl (r ^ n) :=
  ext rfl <| by simp [snd_pow_eq_sum, List.map_const']

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