Commit 2024-08-06 08:17 b1b3aa63

View on Github →

fix: Int.cast_smul_eq_nsmul → Int.cast_smul_eq_zsmul (#15528) This is a recently-introduced typo. The lemma is about ℤ not ℕ.

Estimated changes

Modified Mathlib/Algebra/Lie/Sl2.lean

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

Modified Mathlib/Algebra/Module/Defs.lean

deleted theorem Int.cast_smul_eq_nsmul

added theorem Int.cast_smul_eq_zsmul

modified theorem zsmul_eq_smul_cast

Modified Mathlib/Algebra/Module/Rat.lean

Modified Mathlib/Algebra/Module/Zlattice/Basic.lean

Modified Mathlib/Algebra/Star/CHSH.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/NormedSpace/Connected.lean

Modified Mathlib/Data/ZMod/IntUnitsPower.lean

Modified Mathlib/Data/ZMod/Module.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/Derivation/Basic.lean