Theorems · Theorem · real analysis
NNReal.coe_one
↑1 = 1
- Defined in
- Mathlib.Data.NNReal.Defs
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- NNRealstatement · cited by 4,310
- NNReal.toRealstatement · cited by 1,260
Cited by20
Results whose statement or proof uses this declaration.
- NNReal.toRealHomproof · cited by 13
- NumberField.InfinitePlace.mk_eq_iffproof · cited by 5
- NNReal.coe_eq_oneproof · cited by 5
- BoundedContinuousFunction.norm_compContinuous_leproof · cited by 2
- NNReal.HolderConjugate.conjugate_eqproof · cited by 2
- MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLMproof · cited by 2
- NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplexproof · cited by 1
- NumberField.hermiteTheorem.finite_of_discr_bdd_of_isRealproof · cited by 1
- NNReal.one_le_coeproof · cited by 1
- NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplexproof · cited by 1
- NNReal.holderConjugate_iffproof · cited by 1
- NNReal.holderConjugate_iff_eq_conjExponentproof · cited by 1