Commit 2020-09-25 14:53 10299743

View on Github →

feat(*): finite rings with char = card = n are isomorphic to zmod n (#4234) From the Witt vector project I've made use of the opportunity to remove some unused arguments, and to clean up some code by using namespacing and such.

Estimated changes

Modified src/algebra/char_p.lean

added theorem char_p.cast_card_eq_zero

added theorem char_p_of_ne_zero

added theorem char_p_of_prime_pow_injective

Modified src/data/equiv/ring.lean

added theorem ring_equiv.coe_ring_hom_inj_iff

Modified src/data/fintype/basic.lean

added theorem finset.eq_univ_of_card

added theorem fintype.bijective_iff_injective_and_card

added theorem fintype.bijective_iff_surjective_and_card

modified theorem fintype.card_eq_one_iff

modified def fintype.card_eq_zero_equiv_equiv_pempty

modified theorem fintype.card_eq_zero_iff

modified theorem fintype.card_le_of_injective

modified theorem fintype.card_le_one_iff

modified theorem fintype.card_le_one_iff_subsingleton

modified theorem fintype.card_pos_iff

modified theorem fintype.exists_ne_of_one_lt_card

modified theorem fintype.exists_pair_of_one_lt_card

modified theorem fintype.injective_iff_bijective

modified theorem fintype.injective_iff_surjective

modified theorem fintype.injective_iff_surjective_of_equiv

added theorem fintype.nonempty_equiv_of_card_eq

modified theorem fintype.one_lt_card_iff_nontrivial

modified theorem fintype.surjective_iff_bijective

Modified src/data/zmod/basic.lean

added theorem zmod.cast_hom_bijective

added theorem zmod.cast_hom_injective

modified theorem zmod.ring_hom_eq_of_ker_eq

modified theorem zmod.ring_hom_surjective