Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mem_image_univ_iff_mem_range

Modification history

2020-05-27 01:18

src/data/fintype/basic.lean

feat(ring_theory/fintype): in a finite nonzero_semiring, fintype.card (units R) < fintype.card R (#2793)

Added mem_image_univ_iff_mem_range View on Github →