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)
130@[simp] theorem toComplex_ofLogicRat (q : RationalsFromLogic.LogicRat) :
131 toComplex (ofLogicRat q) = ((RationalsFromLogic.LogicRat.toRat q : ℚ) : ℂ) := by
proof body
Term-mode proof.
132 rw [ofLogicRat, toComplex_ofLogicReal, toReal_ofLogicRat]
133 norm_num
134
135/-- The recovered complex carrier is exactly Mathlib `ℂ`, by transport. -/
depends on (14)
Lean names referenced from this declaration's body.
-
carrier
in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice
decl_use
-
carrier
in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity
decl_use
-
ofLogicRat
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
toComplex_ofLogicReal
in IndisputableMonolith.Foundation.ComplexFromLogic
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
LogicRat
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
toRat
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
ofLogicRat
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
toReal_ofLogicRat
in IndisputableMonolith.Foundation.RealsFromLogic
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
toRat
in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
decl_use