Mathlib Map

Theorems · Theorem · functional analysis

NormOneClass.norm_one

∀ {α : Type u_5} {inst : Norm α} {inst_1 : One α} [self : NormOneClass α], ‖1‖ = 1

The norm of the multiplicative identity is 1.

Defined in
Mathlib.Analysis.Normed.Ring.Basic
Cited by
148 results in Mathlib
Foundations
Depth 86 from the axioms, rests on 1,590 definitions · uses propext, Classical.choice, Quot.sound
Assumes
NormOneClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

norm_algebraMap' · cited by 39norm_algebraMap'NormedSpace.expSeries_radius_eq_top · cited by 27NormedSpace.expSeries_rad…Asymptotics.isLittleO_one_iff · cited by 20Asymptotics.isLittleO_one…nnnorm_one · cited by 11nnnorm_oneComplex.log_one · cited by 7Complex.log_oneAsymptotics.IsLittleO.tendsto_div_nhds_zero · cited by 7IsLittleO.tendsto_div_nhd…Complex.arg_one · cited by 5Complex.arg_oneexists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional · cited by 5exists_nonarchimedean_pow…Complex.norm_cpow_of_imp · cited by 4Complex.norm_cpow_of_impComplex.norm_log_sub_logTaylor_le · cited by 4Complex.norm_log_sub_logT…Asymptotics.isLittleOTVS_one · cited by 4Asymptotics.isLittleOTVS_…PhragmenLindelof.quadrant_I · cited by 4PhragmenLindelof.quadrant…hasSum_geometric_of_norm_lt_one · cited by 4hasSum_geometric_of_norm_…PadicInt.isUnit_iff · cited by 4PadicInt.isUnit_iffComplex.arg_neg_one · cited by 3Complex.arg_neg_oneReal · cited by 25697RealNorm.norm · cited by 5413Norm.normNorm · cited by 512NormNormOneClass · cited by 136NormOneClassNormOneClass.norm_oneCITED BYCITES

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
  • Normstatement and proof · cited by 512
  • NormOneClassstatement and proof · cited by 136

Cited by148

Results whose statement or proof uses this declaration.