Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-27 01:18 2792c93a

View on Github →

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

Estimated changes

Modified src/algebra/associated.lean

modified theorem not_is_unit_zero

Modified src/algebra/gcd_domain.lean

Modified src/algebra/group/units.lean

modified def is_unit

Modified src/algebra/group/units_hom.lean

Modified src/algebra/group_with_zero.lean

Modified src/algebra/ring.lean

Modified src/analysis/asymptotics.lean

Modified src/data/fintype/basic.lean

added theorem card_lt_card_of_injective_of_not_mem

added theorem mem_image_univ_iff_mem_range

Modified src/group_theory/group_action.lean

Modified src/group_theory/monoid_localization.lean

Created src/ring_theory/fintype.lean

added theorem card_units_lt

Modified src/ring_theory/ideals.lean

Modified src/ring_theory/power_series.lean