Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ereal.sign_top

Modification history

2023-02-24 10:27
src/data/real/ereal.lean
refactor(data/real/ereal): add a two-argument induction principle (#18481) …
Modified ereal.sign_topView on Github →
2022-11-30 13:42
src/data/real/ereal.lean
chore(data/real/ereal): fix addition and multiplication on ereal (#17770) …
Added ereal.sign_topView on Github →