Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 21:31 9728bd25

View on Github →

chore(number_theory/number_field): golf int.not_is_field (#12451) Golfed proof of number_theory.number_field.int.not_is_field Co-authored by: David Ang dka31@cantab.ac.uk Co-authored by: Eric Rodriguez ericrboidi@gmail.com Co-authored by: Violeta Hernández vi.hdz.p@gmail.com

Estimated changes