Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 12:54 91dd3b19

View on Github →

chore(ring_theory/integral_domain): dedup, tidy (#13180)

Estimated changes

Modified src/field_theory/finite/basic.lean

Modified src/ring_theory/integral_domain.lean

deleted def field_of_is_domain