Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-11 13:14 8603e6b0

View on Github →

refactor(algebra/associated): rename nonzero_of_irreducible to ne_zero_of_irreducible (#1009)

Estimated changes

Modified src/algebra/associated.lean

added theorem ne_zero_of_irreducible

deleted theorem nonzero_of_irreducible

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/principal_ideal_domain.lean

Modified src/ring_theory/unique_factorization_domain.lean