Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 09:17 6319a238

View on Github →

feat(number_theory/cyclotomic): simplify ne_zeros (#11715) For flt-regular.

Estimated changes

Modified src/algebra/ne_zero.lean

modified theorem ne_zero.of_no_zero_smul_divisors

added theorem ne_zero.trans

Modified src/number_theory/cyclotomic/basic.lean

Modified src/number_theory/cyclotomic/zeta.lean