Commit 2024-05-03 14:30 25896168

View on Github →

perf(NumberTheory.NumberField.Basic): make RingOfIntegers a Type. (#12386) We make 𝓞 K a type rather then a Subalgebra to speed up instances search.

Estimated changes

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

added theorem NumberField.RingOfIntegers.coe_eq_algebraMap

added theorem NumberField.RingOfIntegers.coe_eq_zero_iff

added theorem NumberField.RingOfIntegers.coe_injective

added theorem NumberField.RingOfIntegers.coe_mk

added theorem NumberField.RingOfIntegers.coe_ne_zero_iff

added theorem NumberField.RingOfIntegers.ext

added theorem NumberField.RingOfIntegers.ext_iff

added theorem NumberField.RingOfIntegers.isIntegral

modified theorem NumberField.RingOfIntegers.isIntegral_coe

deleted theorem NumberField.RingOfIntegers.map_mem

added theorem NumberField.RingOfIntegers.map_mk

added theorem NumberField.RingOfIntegers.mk_add_mk

added theorem NumberField.RingOfIntegers.mk_eq_mk

added theorem NumberField.RingOfIntegers.mk_mul_mk

added theorem NumberField.RingOfIntegers.mk_one

added theorem NumberField.RingOfIntegers.mk_sub_mk

added theorem NumberField.RingOfIntegers.mk_zero

added theorem NumberField.RingOfIntegers.neg_mk

added def NumberField.RingOfIntegers.restrict

added def NumberField.RingOfIntegers.restrict_addMonoidHom

added def NumberField.RingOfIntegers.restrict_monoidHom

added def NumberField.RingOfIntegers

modified theorem NumberField.integralBasis_repr_apply

deleted theorem NumberField.isIntegral_of_mem_ringOfIntegers

deleted theorem NumberField.mem_ringOfIntegers

deleted def NumberField.ringOfIntegers

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

modified theorem NumberField.classNumber_eq_one_iff

modified theorem NumberField.exists_ideal_in_class_of_norm_le

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

modified theorem NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/NumberTheory/NumberField/FractionalIdeal.lean

Modified Mathlib/NumberTheory/NumberField/Norm.lean

modified theorem Algebra.coe_trace_int

added theorem RingOfIntegers.algebraMap_norm_algebraMap

added theorem RingOfIntegers.coe_norm

deleted theorem RingOfIntegers.coe_norm_algebraMap

Modified Mathlib/NumberTheory/NumberField/Units/Basic.lean

modified theorem NumberField.Units.coe_pow

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

modified theorem NumberField.Units.dirichletUnitTheorem.seq_ne_zero