prod_add — Mathlib

English

If a ≤ b in FactorSet, then a.prod ≤ b.prod.

Русский

Если a ≤ b в FactorSet, то a.prod ≤ b.prod.

LaTeX

$$$a \le b \Rightarrow a.{prod} \le b.{prod}$$$

Lean4

@[simp]
theorem prod_add : ∀ a b : FactorSet α, (a + b).prod = a.prod * b.prod
  | ⊤, b => show (⊤ + b).prod = (⊤ : FactorSet α).prod * b.prod by simp
  | a, ⊤ => show (a + ⊤).prod = a.prod * (⊤ : FactorSet α).prod by simp
  | WithTop.some a, WithTop.some b => by
    rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]

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