No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
34@[simp] def toReal (r : Rung) : ℝ := (r : ℝ)
proof body
Definition body.
35
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
toComplex
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_im
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_ofLogicReal
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_re
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_re_eq
in IndisputableMonolith.Foundation.LogicComplexCompat
decl_use
-
coshL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
cosL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
expL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
expL_logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
rpowL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
sinhL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
sinL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
sqrtL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_coshL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_cosL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_expL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_logL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_piL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_rpowL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_sinhL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_sinL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
toReal_sqrtL
in IndisputableMonolith.Foundation.LogicRealTranscendentals
decl_use
-
eq_iff_toReal_eq
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
equivReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
fromReal_toReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
le_iff_toReal_le
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
logicReal_recovered_from_completion
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
lt_iff_toReal_lt
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
… and 10 more
depends on (2)
Lean names referenced from this declaration's body.
-
toReal
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
Rung
in IndisputableMonolith.Support.RungFractions
decl_use