Theorems · Theorem · functional analysis
enorm_one
∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] [inst_1 : One G] [NormOneClass G], ‖1‖ₑ = 1- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- ENNReal.ofNNRealproof · cited by 1,279
- ENorm.enormstatement · cited by 715
- NormOneClassstatement and proof · cited by 136
- nnnorm_oneproof · cited by 11
Cited by26
Results whose statement or proof uses this declaration.
- Asymptotics.isLittleOTVS_oneproof · cited by 4
- Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 3
- ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zeroproof · cited by 2
- MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closedproof · cited by 2
- MeasureTheory.integral_of_ae_eq_zero_or_oneproof · cited by 2
- Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zeroproof · cited by 2
- MeasureTheory.measureReal_biUnion_eq_sum_powersetproof · cited by 1
- mem_of_egauge_lt_oneproof · cited by 1
- Real.one_div_one_sub_hasFPowerSeriesOnBall_zeroproof · cited by 1
- Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zeroproof · cited by 1