Lean-Workbook Plus 51434: Logarithmic inequality

For real $a,b,c>0$, $a^{\log c/\log b}=c^{\log a/\log b}$. Real powers and Lean’s total division are used, so $b=1$ is included.

Source: Lean-Workbook row lean_workbook_plus_51434 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.