Commit 2025-07-04 16:39 0a9a9de9

View on Github →

feat(GroupTheory/ArchimedeanDensely): finset.univ of Int AddEquiv is refl or neg (#26741) Follow-up to #24582

Estimated changes

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem Int.card_fintype_addEquiv

added theorem Int.univ_addEquiv