length_product — Mathlib

English

The length of the cross product l1 ×ˢ l2 equals the product of the lengths: length(l1 ×ˢ l2) = length(l1) * length(l2).

Русский

Длина X-произведения l1 ×ˢ l2 равна произведению длин: length(l1 ×ˢ l2) = length(l1) · length(l2).

LaTeX

$$$\operatorname{length}(l_1 ×ˢ l_2) = \operatorname{length}(l_1) \cdot \operatorname{length}(l_2)$$$

Lean4

theorem length_product (l₁ : List α) (l₂ : List β) : length (l₁ ×ˢ l₂) = length l₁ * length l₂ := by
  induction l₁ with
  | nil => exact (Nat.zero_mul _).symm
  | cons x l₁ IH =>
    simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map, Nat.add_comm]

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