isBoundedBilinearMap_mul — Mathlib

English

The map (a,b) ↦ a · b from 𝕜 × 𝕜 to 𝕜 is a bounded bilinear map.

Русский

Отображение (a,b) ↦ a · b: 𝕜 × 𝕜 → 𝕜 является ограниченным билинейным отображением.

LaTeX

$$$IsBoundedBilinearMap 𝕜 \bigl(p \mapsto p.1 \cdot p.2\bigr)$$$

Lean4

theorem isBoundedBilinearMap_mul : IsBoundedBilinearMap 𝕜 fun p : 𝕜 × 𝕜 => p.1 * p.2 :=
  by
  simp_rw [← smul_eq_mul]
  exact isBoundedBilinearMap_smul

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