Theorem SignType.coe_neg

Modification history

2025-07-24 08:42

Mathlib/Data/Sign.lean

chore: split `Data.Sign` (#27232) …

Modified SignType.coe_neg View on Github →

2024-02-27 06:49

Mathlib/Data/Sign.lean

feat(Data/Sign): some more API for `SignType` (#10920) …

Added SignType.coe_neg View on Github →