Commit 2024-03-20 23:42 026dd701

View on Github →

chore: Rename cat_coe_nat/cast_coe_int to cast_natCast/cast_intCast (#11552) Reduce the diff of #11499

Estimated changes

Modified Archive/Imo/Imo2013Q5.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

Modified Mathlib/Algebra/Order/Archimedean.lean

Modified Mathlib/Analysis/InnerProductSpace/OfNorm.lean

Modified Mathlib/Data/Rat/Cast/CharZero.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

deleted theorem Rat.cast_coe_int

deleted theorem Rat.cast_coe_nat

added theorem Rat.cast_intCast

added theorem Rat.cast_natCast

Modified Mathlib/Data/Rat/Floor.lean

Modified Mathlib/Data/Real/Archimedean.lean

Modified Mathlib/Data/Real/Irrational.lean

Modified Mathlib/NumberTheory/DiophantineApproximation.lean

Modified Mathlib/NumberTheory/Harmonic/Bounds.lean

Modified Mathlib/NumberTheory/Harmonic/Int.lean

Modified Mathlib/NumberTheory/Liouville/LiouvilleWith.lean

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean