Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-08 22:28 fdb773a2

View on Github →

chore(algebra/tropical/basic): golf and clean (#10633)

Estimated changes

added theorem tropical.trop_smul
modified theorem tropical.untrop_pow