Commit 2023-12-14 13:12 3465d1aa

View on Github →

feat: Define the dual of a fractional ideal. (#8833) Also moved Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral to Mathlib/NumberTheory/NumberField/Discriminant.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

added theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral

Created Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem FractionalIdeal.coe_dual

added theorem FractionalIdeal.coe_dual_one

added def FractionalIdeal.dual

added theorem FractionalIdeal.dual_div_dual

added theorem FractionalIdeal.dual_dual

added theorem FractionalIdeal.dual_eq_mul_inv

added theorem FractionalIdeal.dual_eq_zero_iff

added theorem FractionalIdeal.dual_injective

added theorem FractionalIdeal.dual_inv

added theorem FractionalIdeal.dual_inv_le

added theorem FractionalIdeal.dual_involutive

added theorem FractionalIdeal.dual_le_dual

added theorem FractionalIdeal.dual_mul_self

added theorem FractionalIdeal.dual_ne_zero

added theorem FractionalIdeal.dual_ne_zero_iff

added theorem FractionalIdeal.dual_zero

added theorem FractionalIdeal.inv_le_dual

added theorem FractionalIdeal.le_dual_iff

added theorem FractionalIdeal.le_dual_inv_aux

added theorem FractionalIdeal.mem_dual

added theorem FractionalIdeal.one_le_dual_one

added theorem FractionalIdeal.self_mul_dual

added theorem Submodule.le_traceDual

added theorem Submodule.le_traceDual_comm

added theorem Submodule.le_traceDual_iff_map_le_one

added theorem Submodule.le_traceDual_mul_iff

added theorem Submodule.le_traceDual_traceDual

added theorem Submodule.mem_traceDual

added theorem Submodule.mem_traceDual_iff_isIntegral

added theorem Submodule.one_le_traceDual_one

added def Submodule.traceDual

added theorem Submodule.traceDual_bot

added theorem Submodule.traceDual_top'

added theorem Submodule.traceDual_top

added theorem isIntegral_discr_mul_of_mem_traceDual

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Discriminant.lean

deleted theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem IsFractionRing.surjective_iff_isField

Modified Mathlib/RingTheory/Trace.lean

added theorem Algebra.trace_ne_zero

added theorem Algebra.trace_surjective