eulerChar_prod — Mathlib

English

Same multiplicativity as above, with a simplified variant: eulerChar 𝕜 (α × β) = eulerChar 𝕜 α · eulerChar 𝕜 β.

Русский

Та же мультипликативность, см. выше: eulerChar 𝕜 (α × β) = eulerChar 𝕜 α · eulerChar 𝕜 β.

LaTeX

$$$ \mathrm{eulerChar}_{𝕜}(\alpha \times \beta) = \mathrm{eulerChar}_{𝕜}(\alpha) \cdot \mathrm{eulerChar}_{𝕜}(\beta) $$$

Lean4

@[simp]
theorem eulerChar_prod [BoundedOrder α] [BoundedOrder β] : eulerChar 𝕜 (α × β) = eulerChar 𝕜 α * eulerChar 𝕜 β := by
  simp [eulerChar, ← mu_prod_mu]

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