Theorem Tropical.add_pow

Modification history

2026-09-02 22:11
Mathlib/Algebra/Tropical/Basic.lean
feat(Algebra/Tropical/Basic): split `Tropical` into `MinTropical`/`MaxTropical` (#42076) …
Deleted Tropical.add_powView on Github →
2024-10-24 21:25
Mathlib/Algebra/Tropical/Basic.lean
feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)
Modified Tropical.add_powView on Github →
2023-01-05 12:49
Mathlib/Algebra/Tropical/Basic.lean
feat: port Algebra.Tropical.Basic (#1165) …
Added Tropical.add_powView on Github →