Commit 2025-03-17 08:40 3040c9b1

View on Github →

feat(Data/Set/Card): Encard multiplication (#22676)

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.toNat_mul

Modified Mathlib/Data/Set/Card.lean

added theorem Set.encard_prod

added theorem Set.ncard_prod

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem ENat.card_prod