Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-02-02 00:53
9d568415
View on Github →
feat(Data/Set/Card):
ncard
/
encard
is strictly monotonic on finite sets (
#34689
)
Estimated changes
Modified
Mathlib/Data/Set/Card.lean
added
theorem
Set.Finite.encard_strictMonoOn
added
theorem
Set.Finite.ncard_strictMonoOn
Modified
Mathlib/GroupTheory/GroupAction/Jordan.lean