rpow_logb_eq_abs — Mathlib

English

For certain structured semirings, there are pass-through equivalences between exponentiation and logarithm-like operations, e.g., rpow_logb_eq_abs expresses a relation linking exponentiation and absolute value.

Русский

Для некоторых структур полуполей существует связь между возведением в степень и логарифмом через модуль/модуль абсолютной величины.

LaTeX

$$$\text{(rpow-logb-abs relation)}$$$

Lean4

theorem rpow_logb_eq_abs (hx : x ≠ 0) : b ^ logb b x = |x| :=
  by
  apply log_injOn_pos
  · simp only [Set.mem_Ioi]
    apply rpow_pos_of_pos b_pos
  · simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]
  rw [log_rpow b_pos, logb, log_abs]
  field_simp [log_ne_zero_of_pos_of_ne_one b_pos b_ne_one]

Похожие утверждения