Commit 2026-01-14 09:35 3aa14e3e

View on Github →

feat(Algebra): MulAction/SMulWithZero by Nat/Int (#33185)

Estimated changes

Modified Mathlib/Algebra/Category/MonCat/Adjunctions.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Module/NatInt.lean

Modified Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean

Modified Mathlib/Algebra/Tropical/Basic.lean

Modified Mathlib/ModelTheory/Arithmetic/Presburger/Basic.lean

Modified Mathlib/Tactic/Abel.lean

modified theorem Mathlib.Tactic.Abel.term_atom