Commit 2025-10-23 09:27 766e19e7

View on Github →

chore: remove MulAction ℚ α → MulAction ℚ≥0 α instances (#30671) This fixes the instances diamond in the NNRat action.

Estimated changes

Modified Mathlib/Algebra/Algebra/Rat.lean

deleted theorem NNRat.cast_smul_eq_nnqsmul

deleted theorem Rat.cast_smul_eq_qsmul

Modified Mathlib/Algebra/Module/Rat.lean

added theorem NNRat.cast_smul_eq_nnqsmul

added theorem Rat.cast_smul_eq_qsmul

Modified Mathlib/Algebra/Order/Module/Rat.lean

Modified Mathlib/Data/NNRat/Lemmas.lean