house_mul_le — Mathlib

English

The house is submultiplicative with respect to multiplication: house(αβ) ≤ house(α) · house(β).

Русский

Домашняя функция удовлетворяет неравенству на произведение: house(αβ) ≤ house(α) · house(β).

LaTeX

$$$\\operatorname{house}(αβ) \\le \\operatorname{house}(α) \\cdot \\operatorname{house}(β).$$$

Lean4

theorem house_mul_le (α β : K) : house (α * β) ≤ house α * house β := by simp only [house, map_mul]; apply norm_mul_le

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