621 intro a b hab 622 -- Translate to powers. 623 rw [embed_eq_pow, embed_eq_pow] at hab 624 -- Take logs. 625 have hpos_a : 0 < γ.value ^ (LogicNat.toNat a) := pow_pos γ.pos _ 626 have hpos_b : 0 < γ.value ^ (LogicNat.toNat b) := pow_pos γ.pos _ 627 have hlog : Real.log (γ.value ^ (LogicNat.toNat a)) 628 = Real.log (γ.value ^ (LogicNat.toNat b)) := by 629 exact congrArg Real.log hab 630 rw [Real.log_pow, Real.log_pow] at hlog 631 -- Cancel the non-zero log γ.value. 632 have hne := log_generator_ne_zero γ 633 have hcast : ((LogicNat.toNat a : ℝ)) = ((LogicNat.toNat b : ℝ)) := by 634 have := mul_right_cancel₀ hne hlog 635 exact this 636 have h_nat : LogicNat.toNat a = LogicNat.toNat b := by exact_mod_cast hcast 637 -- Lift back to LogicNat via the equivalence. 638 have := congrArg LogicNat.fromNat h_nat 639 rw [LogicNat.fromNat_toNat, LogicNat.fromNat_toNat] at this 640 exact this 641 642/-! ## Order via the Embedding (γ > 1 case) 643 644When `γ > 1`, the orbit is strictly increasing under multiplication 645by `γ`, and `embed γ` is a strictly monotone embedding of the Peano 646order on `LogicNat` into `(ℝ, ≤)`. This is the analytic counterpart 647of the abstract Peano order from Section 5b. -/ 648 649/-- For `γ > 1`, `γⁿ ≤ γᵐ ↔ n ≤ m` on `Nat`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.