Theorem self_mul_sign

Modification history

2025-07-24 08:42

Mathlib/Data/Sign.lean

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

Modified self_mul_sign View on Github →

2024-04-24 13:42

Mathlib/Data/Sign.lean

refactor(QuadraticForm/Real): migrate to `SignType` (#12319) …

Added self_mul_sign View on Github →