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)
562@[simp] theorem embed_succ (γ : Generator) (n : LogicNat) :
563 embed γ (LogicNat.succ n) = γ.value * embed γ n := rfl
proof body
Term-mode proof.
564
565/-- The embedding lands in the strictly positive reals. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
embed_add
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
depends on (7)
Lean names referenced from this declaration's body.
-
embed
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
Generator
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
succ
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
embed
in IndisputableMonolith.Foundation.HamiltonianEmergence
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
succ
in IndisputableMonolith.RRF.Core.Vantage
decl_use