Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-02 15:21 17747c09

View on Github →

feat(number_theory): define number fields, function fields and their rings of integers (#8701) Co-Authored-By: Ashvni ashvni.n@gmail.com

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem char_zero.of_algebra

Modified src/algebraic_geometry/structure_sheaf.lean

Created src/number_theory/function_field.lean

added def function_field.ring_of_integers

added def function_field

Created src/number_theory/number_field.lean

added theorem number_field.ring_of_integers.is_integral_coe

added def number_field.ring_of_integers

Modified src/ring_theory/integrally_closed.lean

added theorem integral_closure.is_integrally_closed_of_finite_extension

Modified src/ring_theory/localization.lean

deleted theorem is_localization.epic_of_localization_map

added theorem is_localization.monoid_hom_ext

added theorem is_localization.ring_hom_ext