Theorems · Definition · number theory
WithZeroMulInt.toNNReal
{e : NNReal} → e ≠ 0 → WithZero (Multiplicative ℤ) →*₀ NNRealGiven a nonzero e : ℝ≥0, this is the map ℤᵐ⁰ → ℝ≥0 sending 0 ↦ 0 and
x ↦ e^(WithZero.unzero hx).toAdd when x ≠ 0 as a MonoidWithZeroHom.
- Defined in
- Mathlib.Data.Int.WithZero
- Cited by
- 28 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- NNRealstatement and proof · cited by 4,310
- Multiplicativestatement and proof · cited by 875
- MonoidWithZeroHomstatement · cited by 704
- WithZerostatement and proof · cited by 586
- Multiplicative.toAddproof · cited by 161
- WithZero.unzeroproof · cited by 38
Cited by30
Results whose statement or proof uses this declaration.
- NumberField.FinitePlace.norm_embeddingproof · cited by 6
- WithZeroMulInt.toNNReal_strictMonostatement and proof · cited by 4
- NumberField.HeightOneSpectrum.adicAbv_defstatement · cited by 4
- IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMapproof · cited by 3
- WithZeroMulInt.toNNReal_neg_applystatement · cited by 2
- NumberField.HeightOneSpectrum.rankOne_hom'_defstatement · cited by 2
- NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbvstatement · cited by 2
- WithZeroMulInt.toNNReal_le_one_iffstatement and proof · cited by 1
- WithZeroMulInt.toNNReal_lt_one_iffstatement and proof · cited by 1
- WithZeroMulInt.toNNReal_ne_zerostatement and proof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.intAdicAbvDefproof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDefproof · cited by 1