Theorems · Theorem · functional analysis
norm_mul_le
∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖The norm is submultiplicative.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonUnitalSeminormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement · cited by 5,413
- NonUnitalSeminormedRingstatement and proof · cited by 44
- NonUnitalSeminormedRing.norm_mul_leproof · cited by 1
Cited by32
Results whose statement or proof uses this declaration.
- CStarRing.norm_star_mul_selfproof · cited by 16
- nnnorm_mul_leproof · cited by 4
- multipliable_one_add_of_summableproof · cited by 4
- Asymptotics.isBigOWith_const_mul_selfproof · cited by 4
- EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsumproof · cited by 3
- Asymptotics.isBigOWith_of_eq_mulproof · cited by 3
- Asymptotics.IsBigOWith.mulproof · cited by 3
- summable_norm_mul_geometric_of_norm_lt_oneproof · cited by 2
- norm_commutator_units_sub_one_leproof · cited by 2
- Summable.mul_normproof · cited by 2
- balancedHull.balancedproof · cited by 2
- one_le_norm_oneproof · cited by 2