Lean-Workbook Plus 20863: Logarithmic identity

For all real $a,b,c,d$, $(\log b/\log a)(\log d/\log c)=(\log b/\log c)(\log d/\log a)$. These are ratios of Lean’s total real logarithm, with division by zero defined as zero; the claim does not require ordinary logarithmic bases to be valid.

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