Theorem sign_intCast

Modification history

2025-07-24 08:42
Mathlib/Data/Sign.lean
chore: split `Data.Sign` (#27232) …
Modified sign_intCastView on Github →
2025-04-04 17:16
Mathlib/Data/Sign.lean
chore: use mixin ordered algebraic typeclasses (part 1) (#20594)
Modified sign_intCastView on Github →
2025-03-17 06:31
Mathlib/Data/Sign.lean
chore: Migrate to `DecidableLT` and `DecidableLE` (#22238) …
Modified sign_intCastView on Github →
2024-05-13 21:00
Mathlib/Data/Sign.lean
feat(NumberTheory/LSeries): Odd Hurwitz zeta functions (#12779) …
Added sign_intCastView on Github →