Theorem Set.SMulAntidiagonal.eq_of_fst_eq_fst

Modification history

2026-04-28 01:10

Mathlib/Data/Set/SMulAntidiagonal.lean

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

Modified Set.SMulAntidiagonal.eq_of_fst_eq_fst View on Github →

2024-07-21 23:44

Mathlib/Data/Set/SMulAntidiagonal.lean

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

Added Set.SMulAntidiagonal.eq_of_fst_eq_fst View on Github →