English
In a normed division ring, the sub-multiplicative norm is actually strictly multiplicative with respect to scalar multiplication: ∥r • x∥ = ∥r∥ ∥x∥ for all r,x.
Русский
В нормированном делимом кольце нормa подмножества на самом деле строгопритяжена к умножению: ∥r • x∥ = ∥r∥ ∥x∥ для всех r,x.
LaTeX
$$$$\\|r \\cdot x\\| = \\|r\\| \\cdot \\|x\\|.$$$$
Lean4
/-- For a normed division ring, a sub-multiplicative norm is actually strictly multiplicative.
This is not an instance as it forms a loop with `NormSMulClass.toIsBoundedSMul`. -/
theorem toNormSMulClass : NormSMulClass α β where
norm_smul r
x := by
by_cases h : r = 0
· simp [h, zero_smul α x]
· refine le_antisymm (norm_smul_le r x) ?_
calc
‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
_ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
_ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
