Commit 2023-09-25 00:55 2517504a

View on Github →

chore: add IsROrC.toDecidableEq (#7315) We already have noncomputable DecidableEq instances for Real and Complex; putting them here too reduces friction in code generalized to IsROrC K.

Estimated changes