Commit 2023-10-26 17:29 9e92f67f

View on Github →

feat(Data/*/Sqrt): decidability of IsSquare (#7935) Zulip thread

Estimated changes

added theorem even_ofMul_iff
added theorem even_toAdd_iff
added theorem isSquare_ofAdd_iff
modified theorem isSquare_op_iff
added theorem isSquare_toMul_iff
added theorem isSquare_unop_iff