Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-05 12:11 34e366c6

View on Github →

refactor(*): remove uses of @[class] def (#6028) Preparation for lean 4, which does not support this idiom.

Estimated changes

modified theorem is_galois.integral
deleted theorem is_galois.normal
modified theorem is_galois.separable
added theorem is_galois.splits
deleted def is_galois
added theorem is_galois_iff
modified theorem normal.is_integral
added theorem normal.out
modified theorem normal.splits
deleted def normal
added theorem normal_iff