Commit 2024-09-24 08:53 2d315a52

View on Github →

feat(CharP): Int.cast is injective on Ico 0 p (#17063) and generalise Fin.charP

Estimated changes

modified theorem Fin.natCast_self