Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-03 22:25 641b6a82

View on Github →

feat(number_theory/number_field/basic): add integral_basis (#18474)

Estimated changes

Modified src/number_theory/number_field/basic.lean

added theorem number_field.integral_basis_apply

modified theorem number_field.ring_of_integers.not_is_field

added theorem number_field.ring_of_integers.rank

Modified src/ring_theory/dedekind_domain/integral_closure.lean

added theorem is_integral_closure.is_localization

added theorem is_integral_closure.module_free

added theorem is_integral_closure.rank

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_closure.no_zero_smul_divisors