Theorem sign_intCast

Modification history

2025-04-04 17:16

Mathlib/Data/Sign.lean

chore: use mixin ordered algebraic typeclasses (part 1) (#20594)

Modified sign_intCast View on Github →

2025-03-17 06:31

Mathlib/Data/Sign.lean

chore: Migrate to `DecidableLT` and `DecidableLE` (#22238) …

Modified sign_intCast View on Github →

2024-05-13 21:00

Mathlib/Data/Sign.lean

feat(NumberTheory/LSeries): Odd Hurwitz zeta functions (#12779) …

Added sign_intCast View on Github →