Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-20 09:53 2f548407

View on Github →

refactor(*): replace comm_ring/integral_domain with ring/domain where possible (#9739)

Estimated changes

Modified src/algebra/algebra/subalgebra.lean

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/integral_normalization.lean

Modified src/data/polynomial/mirror.lean

modified theorem polynomial.mirror_mul_of_domain

modified theorem polynomial.mirror_smul

Modified src/data/polynomial/reverse.lean

modified theorem polynomial.trailing_coeff_mul

Modified src/data/polynomial/ring_division.lean

Modified src/data/real/cau_seq.lean

Modified src/field_theory/fixed.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/free_module/pid.lean

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

Modified src/ring_theory/hahn_series.lean

modified theorem hahn_series.order_mul

Modified src/ring_theory/ideal/basic.lean

modified theorem ideal.bot_prime

Modified src/ring_theory/ideal/operations.lean

modified theorem ring_hom.ker_is_prime

Modified src/ring_theory/localization.lean

Modified src/ring_theory/power_series/basic.lean