Mathlib Map

Theorems · Theorem · real analysis

NNReal.sqrt_zero

NNReal.sqrt 0 = 0
Defined in
Mathlib.Analysis.Real.Sqrt
Cited by
9 results in Mathlib
Foundations
Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Real.sqrt_zero · cited by 28Real.sqrt_zeroReal.sqrt_eq_zero_of_nonpos · cited by 12Real.sqrt_eq_zero_of_nonp…CFC.sqrt_eq_cfc · cited by 5CFC.sqrt_eq_cfcNNReal.sqrtHom · cited by 3NNReal.sqrtHomReal.sqrt_prod · cited by 1Real.sqrt_prodProbabilityTheory.Kernel.HasSubgaussianMGF.add · cited by 1HasSubgaussianMGF.addCFC.continuousOn_sqrt · cited by 1CFC.continuousOn_sqrtNNReal.agm_zero_left · cited by 1NNReal.agm_zero_leftCFC.sqrt_rpow · cited by 0CFC.sqrt_rpowCFC.sqrt_rpow_nnreal · cited by 0CFC.sqrt_rpow_nnrealDFunLike.coe · cited by 62936DFunLike.coeNNReal · cited by 4310NNRealOrderIso · cited by 874OrderIsoNNReal.sqrt · cited by 91NNReal.sqrtNNReal.sqrt_zeroCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by10

Results whose statement or proof uses this declaration.