Theorem Finset.smulAntidiagonal_mono_right

Modification history

2026-04-28 01:10

Mathlib/Data/Finset/SMulAntidiagonal.lean

refactor(Algebra/MonoidAlgebra/PointwiseSMul): switch action from Finsupp to (Add)MonoidAlgebra and multiplicativize (#35243) …

Modified Finset.smulAntidiagonal_mono_right View on Github →

2024-07-21 23:44

Mathlib/Data/Finset/SMulAntidiagonal.lean

feat (Algebra/Order/AddTorsor) : Antidiagonals for SMul and VAdd, with finiteness properties (#14479) …

Added Finset.smulAntidiagonal_mono_right View on Github →