English
For any base b and any natural n with n ≥ 2, the logarithm of the natural embedding of n equals the natural logarithm of n, both computed in the ambient semifield. Equivalently, log_b(ofNat(n)) = Nat.log b ofNat(n).
Русский
Для любого основания b и натурального n с n ≥ 2 логарифм числа n, воспринятого как элемент поля, равенNat.log b n, приведённому к тому же полю.
LaTeX
$$$\log_b\bigl(\text{ofNat}(n)\bigr) = \mathrm{Nat\log}\, b\, \text{ofNat}(n)\;\;\; (n \ge 2)$$$
Lean4
@[simp]
theorem log_ofNat (b : ℕ) (n : ℕ) [n.AtLeastTwo] : log b (ofNat(n) : R) = Nat.log b ofNat(n) :=
log_natCast b n
