Commit 2024-08-07 14:38 e2938e09

View on Github →

chore: backports for leanprover/lean4#4814 (part 29) (#15572)

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

modified theorem contMDiffOn_openEmbedding_symm

modified theorem contMDiff_openEmbedding

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

modified theorem FractionalIdeal.coe_dual

modified theorem FractionalIdeal.dual_le_dual

modified theorem FractionalIdeal.dual_mul_self

modified theorem FractionalIdeal.dual_ne_zero

modified theorem FractionalIdeal.le_dual_iff

modified theorem FractionalIdeal.le_dual_inv_aux

modified theorem FractionalIdeal.mem_dual

modified theorem FractionalIdeal.self_mul_dual

modified theorem map_equiv_traceDual

Modified Mathlib/RingTheory/Ideal/Norm.lean

modified theorem Ideal.exists_mul_add_mem_pow_succ

modified theorem Ideal.mul_add_mem_pow_succ_unique

modified theorem cardQuot_pow_of_prime

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

modified theorem Algebra.map_intNormAux