Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-24 00:18 d57ac08c

View on Github →

feat(field_theory/separable): definition and basic properties (#3155)

Estimated changes

Created src/field_theory/separable.lean

added theorem polynomial.separable.mul

added theorem polynomial.separable.of_mul_left

added theorem polynomial.separable.of_mul_right

added def polynomial.separable

added theorem polynomial.separable_X

added theorem polynomial.separable_X_add_C

added theorem polynomial.separable_def'

added theorem polynomial.separable_def

added theorem polynomial.separable_one

Modified src/ring_theory/coprime.lean

added theorem is_coprime.add_mul_left_left

added theorem is_coprime.add_mul_left_left_iff

added theorem is_coprime.add_mul_left_right

added theorem is_coprime.add_mul_left_right_iff

added theorem is_coprime.add_mul_right_left

added theorem is_coprime.add_mul_right_left_iff

added theorem is_coprime.add_mul_right_right

added theorem is_coprime.add_mul_right_right_iff

added theorem is_coprime.mul_add_left_left

added theorem is_coprime.mul_add_left_left_iff

added theorem is_coprime.mul_add_left_right

added theorem is_coprime.mul_add_left_right_iff

added theorem is_coprime.mul_add_right_left

added theorem is_coprime.mul_add_right_left_iff

added theorem is_coprime.mul_add_right_right

added theorem is_coprime.mul_add_right_right_iff

added theorem is_coprime.of_add_mul_left_left

added theorem is_coprime.of_add_mul_left_right

added theorem is_coprime.of_add_mul_right_left

added theorem is_coprime.of_add_mul_right_right

added theorem is_coprime.of_mul_add_left_left

added theorem is_coprime.of_mul_add_left_right

added theorem is_coprime.of_mul_add_right_left

added theorem is_coprime.of_mul_add_right_right