Mathlib Map

Theorems · Theorem · special functions

Real.arccos_eq_zero

∀ {x : ℝ}, Real.arccos x = 0 ↔ 1 ≤ x
Defined in
Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Cited by
1 results in Mathlib
Foundations
Depth 198 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.

InnerProductGeometry.angle_eq_zero_iff · cited by 5InnerProductGeometry.angl…Real · cited by 25697RealReal.arccos · cited by 90Real.arccosReal.arccos_eq_zeroCITED BYCITES

Cites2

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

  • Realstatement and proof · cited by 25,697
  • Real.arccosstatement · cited by 90

Cited by1

Results whose statement or proof uses this declaration.