Commit 2024-05-07 23:13 424683e8

View on Github →

chore: Rename smul_one_eq_coe to smul_one_eq_cast (#12621)

Estimated changes

Modified Archive/Wiedijk100Theorems/FriendshipGraphs.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/Field/Defs.lean

added theorem NNRat.smul_one_eq_cast

deleted theorem NNRat.smul_one_eq_coe

added theorem Rat.smul_one_eq_cast

deleted theorem Rat.smul_one_eq_coe

Modified Mathlib/Algebra/Module/BigOperators.lean

Modified Mathlib/Algebra/Module/Defs.lean

added theorem Int.smul_one_eq_cast

deleted theorem Int.smul_one_eq_coe

added theorem Nat.smul_one_eq_cast

deleted theorem Nat.smul_one_eq_coe

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Algebra/Polynomial/UnitTrinomial.lean

Modified Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/Normed/Group/AddCircle.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean