Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-11-05 17:58
8eac03c6
View on Github →
feat(algebra/char_p): define the characteristic of a semiring
Estimated changes
Created
algebra/char_p.lean
added
theorem
add_pow_char
added
theorem
char_p.cast_eq_zero
added
theorem
char_p.eq
added
theorem
char_p.exists
added
theorem
char_p.exists_unique
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
is_monoid_hom.map_frobenius
added
theorem
ring_char.eq
added
theorem
ring_char.spec
Modified
algebra/group_power.lean
added
theorem
pow_eq_zero