Commit 2024-05-28 07:17 3e7433cb

View on Github →

chore: Rename more coe_nat/coe_int to natCast/intCast (#13205)

Estimated changes

Modified Archive/Imo/Imo2008Q3.lean

Modified Mathlib/Algebra/BigOperators/Ring.lean

deleted theorem Finset.prod_range_cast_nat_sub

added theorem Finset.prod_range_natCast_sub

Modified Mathlib/Algebra/Order/Group/Int.lean

deleted theorem Int.coe_nat_strictMono

added theorem Int.natCast_strictMono

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

deleted theorem Polynomial.ringHom_eval₂_cast_int_ringHom

added theorem Polynomial.ringHom_eval₂_intCastRingHom

Modified Mathlib/Algebra/Polynomial/Eval.lean

deleted theorem Polynomial.cast_int_comp

added theorem Polynomial.intCast_comp

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

deleted theorem Real.Angle.coe_int_mul_eq_zsmul

deleted theorem Real.Angle.coe_nat_mul_eq_nsmul

added theorem Real.Angle.intCast_mul_eq_zsmul

added theorem Real.Angle.natCast_mul_eq_nsmul

modified theorem Real.Angle.two_nsmul_coe_pi

modified theorem Real.Angle.two_zsmul_coe_pi

Modified Mathlib/Data/Finite/Card.lean

added theorem PartENat.card_eq_coe_natCard

deleted theorem PartENat.card_eq_coe_nat_card

Modified Mathlib/Data/Int/Cast/Lemmas.lean

deleted theorem Commute.cast_int_left

deleted theorem Commute.cast_int_mul_cast_int_mul

deleted theorem Commute.cast_int_mul_left

deleted theorem Commute.cast_int_mul_right

deleted theorem Commute.cast_int_mul_self

deleted theorem Commute.cast_int_right

added theorem Commute.intCast_left

added theorem Commute.intCast_mul_intCast_mul

added theorem Commute.intCast_mul_left

added theorem Commute.intCast_mul_right

added theorem Commute.intCast_mul_self

added theorem Commute.intCast_right

deleted theorem Commute.self_cast_int_mul

deleted theorem Commute.self_cast_int_mul_cast_int_mul

added theorem Commute.self_intCast_mul

added theorem Commute.self_intCast_mul_intCast_mul

added theorem Int.cast_dvd_cast

deleted theorem Int.coe_int_dvd

deleted theorem SemiconjBy.cast_int_mul_cast_int_mul

deleted theorem SemiconjBy.cast_int_mul_left

deleted theorem SemiconjBy.cast_int_mul_right

added theorem SemiconjBy.intCast_mul_intCast_mul

added theorem SemiconjBy.intCast_mul_left

added theorem SemiconjBy.intCast_mul_right

Modified Mathlib/Data/Int/Defs.lean

deleted theorem Int.coe_nat_pow

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Int/SuccPred.lean

added theorem Int.natCast_covBy

deleted theorem Nat.cast_int_covBy_iff

Modified Mathlib/Data/Nat/Cast/Commute.lean

deleted theorem Commute.cast_nat_mul_cast_nat_mul

deleted theorem Commute.cast_nat_mul_left

deleted theorem Commute.cast_nat_mul_right

deleted theorem Commute.cast_nat_mul_self

added theorem Commute.natCast_mul_left

added theorem Commute.natCast_mul_natCast_mul

added theorem Commute.natCast_mul_right

added theorem Commute.natCast_mul_self

deleted theorem Commute.self_cast_nat_mul

deleted theorem Commute.self_cast_nat_mul_cast_nat_mul

added theorem Commute.self_natCast_mul

added theorem Commute.self_natCast_mul_natCast_mul

deleted theorem SemiconjBy.cast_nat_mul_cast_nat_mul

deleted theorem SemiconjBy.cast_nat_mul_left

deleted theorem SemiconjBy.cast_nat_mul_right

added theorem SemiconjBy.natCast_mul_left

added theorem SemiconjBy.natCast_mul_natCast_mul

added theorem SemiconjBy.natCast_mul_right

Modified Mathlib/Data/Nat/ModEq.lean

Modified Mathlib/Data/Real/Irrational.lean

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.intCast_eq_iff

deleted theorem ZMod.int_coe_ringEquivCongr

deleted theorem ZMod.int_coe_zmod_eq_iff

added theorem ZMod.natCast_eq_iff

deleted theorem ZMod.nat_coe_zmod_eq_iff

added theorem ZMod.ringEquivCongr_intCast

Modified Mathlib/Dynamics/Ergodic/AddCircle.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

Modified Mathlib/NumberTheory/Liouville/Basic.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

deleted theorem LucasLehmer.Int.coe_nat_pow_pred

added theorem LucasLehmer.Int.natCast_pow_pred

added theorem LucasLehmer.X.fst_intCast

added theorem LucasLehmer.X.fst_natCast

deleted theorem LucasLehmer.X.int_coe_fst

deleted theorem LucasLehmer.X.int_coe_snd

deleted theorem LucasLehmer.X.nat_coe_fst

deleted theorem LucasLehmer.X.nat_coe_snd

added theorem LucasLehmer.X.snd_intCast

added theorem LucasLehmer.X.snd_natCast

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

deleted theorem Zsqrtd.coe_int_dvd_coe_int

deleted theorem Zsqrtd.coe_int_dvd_iff

added theorem Zsqrtd.intCast_dvd

added theorem Zsqrtd.intCast_dvd_intCast

Modified Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

Modified Mathlib/Order/Atoms/Finite.lean

Modified Mathlib/Order/Grade.lean

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

Modified Mathlib/Tactic/NormNum/GCD.lean

Modified Mathlib/Tactic/ReduceModChar.lean

deleted theorem Tactic.ReduceModChar.CharP.cast_int_eq_mod

added theorem Tactic.ReduceModChar.CharP.intCast_eq_mod