Commit 2023-03-14 08:11 3b70fc67

View on Github →

feat: port Algebra.CharP.Basic (#2845)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharP/Basic.lean

added theorem CharP.addOrderOf_one

added theorem CharP.cast_card_eq_zero

added theorem CharP.cast_eq_mod

added theorem CharP.cast_eq_zero

added theorem CharP.cast_eq_zero_iff

added theorem CharP.charP_to_charZero

added theorem CharP.char_is_prime

added theorem CharP.char_is_prime_of_pos

added theorem CharP.char_is_prime_of_two_le

added theorem CharP.char_is_prime_or_zero

added theorem CharP.char_ne_one

added theorem CharP.char_ne_zero_of_finite

added theorem CharP.congr

added theorem CharP.eq

added theorem CharP.exists

added theorem CharP.exists_unique

added theorem CharP.false_of_nontrivial_of_char_one

added theorem CharP.int_cast_eq_int_cast_iff

added theorem CharP.int_cast_eq_zero_iff

added theorem CharP.neg_one_ne_one

added theorem CharP.neg_one_pow_char

added theorem CharP.neg_one_pow_char_pow

added theorem CharP.nontrivial_of_char_ne_one

added theorem CharP.pow_prime_pow_mul_eq_one_iff

added theorem CharP.ringChar_ne_one

added theorem CharP.ringChar_ne_zero_of_finite

added theorem CharP.ringChar_of_prime_eq_zero

added theorem Int.cast_injOn_of_ringChar_ne_two

added theorem MonoidHom.iterate_map_frobenius

added theorem MonoidHom.map_frobenius

added theorem MonoidHom.map_iterate_frobenius

added theorem NeZero.not_char_dvd

added theorem NeZero.of_not_dvd

added theorem Ring.eq_self_iff_eq_zero_of_char_ne_two

added theorem Ring.neg_one_ne_one_of_char_ne_two

added theorem RingHom.charP_iff_charP

added theorem RingHom.iterate_map_frobenius

added theorem RingHom.map_frobenius

added theorem RingHom.map_iterate_frobenius

added theorem add_pow_char

added theorem add_pow_char_of_commute

added theorem add_pow_char_pow

added theorem add_pow_char_pow_of_commute

added theorem charP_of_ne_zero

added theorem charP_of_prime_pow_injective

added theorem eq_iff_modEq_int

added def frobenius

added theorem frobenius_add

added theorem frobenius_def

added theorem frobenius_inj

added theorem frobenius_mul

added theorem frobenius_nat_cast

added theorem frobenius_neg

added theorem frobenius_one

added theorem frobenius_sub

added theorem frobenius_zero

added theorem isSquare_of_charTwo'

added theorem iterate_frobenius

added theorem list_sum_pow_char

added theorem multiset_sum_pow_char

added theorem ringChar.Nat.cast_ringChar

added theorem ringChar.dvd

added theorem ringChar.eq

added theorem ringChar.eq_iff

added theorem ringChar.eq_zero

added theorem ringChar.of_eq

added theorem ringChar.spec

added theorem sub_pow_char

added theorem sub_pow_char_of_commute

added theorem sub_pow_char_pow

added theorem sub_pow_char_pow_of_commute

added theorem sum_pow_char

Modified Mathlib/Data/Int/Cast/Basic.lean

added theorem Int.int_cast_ofNat

Modified Mathlib/Data/ULift.lean

added theorem ULift.ext_iff