Theorem Set.encard_inv

Modification history

2024-12-01 00:08
Mathlib/Algebra/Group/Pointwise/Set/Card.lean
feat: introduce ENat.card, and use it in place of PartENat.card (#19624)
Modified Set.encard_invView on Github →
2024-11-23 15:57
Mathlib/Algebra/Group/Pointwise/Set/Card.lean
feat: `s⁻¹.encard = s.encard` (#19400) …
Added Set.encard_invView on Github →