Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-27 19:21 aa0b274b

View on Github →

chore(*): split lines and move module doc measure_theory/category/Meas (#6459)

Estimated changes

Modified src/deprecated/subgroup.lean

Modified src/deprecated/subring.lean

Modified src/field_theory/chevalley_warning.lean

Modified src/field_theory/finite/basic.lean

modified theorem finite_field.card_image_polynomial_eval

Modified src/field_theory/fixed.lean

Modified src/field_theory/intermediate_field.lean

Modified src/field_theory/primitive_element.lean

Modified src/field_theory/splitting_field.lean

modified theorem polynomial.factor_dvd_of_nat_degree_ne_zero

Modified src/field_theory/subfield.lean

Modified src/measure_theory/category/Meas.lean

Modified src/ring_theory/ideal/operations.lean

Modified src/ring_theory/principal_ideal_domain.lean