Commit 2026-11-10 17:26 68dd2955

View on Github →

chore: correct naming of coercion lemmas about coeIdeal (#45832) Refer to it as coeIdeal, not coe or coe_ideal.

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

deleted theorem FractionalIdeal.count_coe

added theorem FractionalIdeal.count_coeIdeal

added theorem FractionalIdeal.count_coeIdeal_nonneg

deleted theorem FractionalIdeal.count_coe_nonneg

deleted theorem Ideal.finprod_heightOneSpectrum_factorization_coe

added theorem Ideal.finprod_heightOneSpectrum_factorization_coeIdeal

deleted theorem Ideal.hasFiniteMulSupport_coe

added theorem Ideal.hasFiniteMulSupport_coeIdeal

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

added theorem FractionalIdeal.coeIdeal_mul_inv

deleted theorem FractionalIdeal.coe_ideal_mul_inv

added theorem FractionalIdeal.one_mem_inv_coeIdeal

deleted theorem FractionalIdeal.one_mem_inv_coe_ideal

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/FractionalIdeal/Inverse.lean

added theorem FractionalIdeal.coeIdeal_le_self_mul_inv

added theorem FractionalIdeal.coeIdeal_span_singleton_div_self

added theorem FractionalIdeal.coeIdeal_span_singleton_inv_mul

added theorem FractionalIdeal.coeIdeal_span_singleton_mul_inv

deleted theorem FractionalIdeal.coe_ideal_le_self_mul_inv

deleted theorem FractionalIdeal.coe_ideal_span_singleton_div_self

deleted theorem FractionalIdeal.coe_ideal_span_singleton_inv_mul

deleted theorem FractionalIdeal.coe_ideal_span_singleton_mul_inv