Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-14 10:07
e2860129
View on Github →
feat(algebra/ne_zero):
pos_of_ne_zero_coe
(
#11437
)
Estimated changes
Modified
src/algebra/ne_zero.lean
added
theorem
ne_zero.not_char_dvd
deleted
theorem
ne_zero.not_dvd_char
added
theorem
ne_zero.pos_of_ne_zero_coe
Modified
src/ring_theory/polynomial/cyclotomic/basic.lean