Theorem sign_mul_self

Modification history

2025-07-24 08:42

Mathlib/Data/Sign.lean

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

Modified sign_mul_self View on Github →

2024-04-24 13:42

Mathlib/Data/Sign.lean

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

Added sign_mul_self View on Github →