Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 05:12 47e2f804

View on Github →

chore(*): Replace integral_domain assumptions with no_zero_divisors (#5877) This removes unnecessary nontrivial assumptions, and reduces some comm_ring requirements to comm_semiring. This also adds some missing nontrivial and no_zero_divisors instances.

Estimated changes

Modified src/algebra/algebra/subalgebra.lean

Modified src/algebra/char_p/basic.lean

modified theorem frobenius_inj

Modified src/algebra/opposites.lean

Modified src/algebra/polynomial/big_operators.lean

modified theorem polynomial.nat_degree_prod

Modified src/data/multiset/basic.lean

modified theorem multiset.prod_ne_zero

Modified src/data/polynomial/degree/definitions.lean

modified theorem polynomial.degree_pow

modified theorem polynomial.leading_coeff_X_add_C

Modified src/data/quaternion.lean

modified theorem quaternion.conj_fixed

modified theorem quaternion_algebra.conj_fixed

Modified src/linear_algebra/linear_independent.lean

modified theorem linear_independent_monoid_hom

Modified src/ring_theory/prime.lean

Modified src/ring_theory/subring.lean

Modified src/ring_theory/subsemiring.lean