Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 01:49 61d2ad05

View on Github →

chore(algebra/char_p/basic): uniformise notation and weaken some assumptions (#6765) I had looked at this file in an earlier PR and decided to come back to uniformise the notation, using always R and never α for the generic type of the file. While I was at it, I started also changing

  • some semiring assumptions to add_monoid + has_one,
  • some ring assumptions to add_group + has_one. In the long run, I think that the characteristic of a ring should be defined as the order of 1 in the additive submonoid, but this is not what I am doing at the moment! Here is a related Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/char_zero

Estimated changes

modified theorem add_pow_char
modified theorem add_pow_char_of_commute
modified theorem add_pow_char_pow
modified theorem add_pow_char_pow_of_commute
modified theorem char_p.cast_card_eq_zero
modified theorem char_p.cast_eq_mod
modified theorem char_p.cast_eq_zero
modified theorem char_p.char_p_to_char_zero
modified theorem char_p.eq
modified theorem char_p.exists
modified theorem char_p.exists_unique
modified theorem char_p.int_cast_eq_zero_iff
modified theorem char_p.neg_one_ne_one
modified theorem char_p.ring_char_ne_one
modified theorem eq_iff_modeq_int
modified theorem frobenius_inj
modified theorem sub_pow_char
modified theorem sub_pow_char_of_commute
modified theorem sub_pow_char_pow
modified theorem sub_pow_char_pow_of_commute
modified theorem perfection_map.map_eq_map