Deprecated

@[deprecated Set.SMulAntidiagonal.finite_of_finite_fst (since := "2026-02-13")]

theorem Finsupp.finite_vaddAntidiagonal {G : Type u_1} {P : Type u_2} {s : Set G} [SMul G P] [IsLeftCancelSMul G P] (hs : s.Finite) (t : Set P) (p : P) : (s.smulAntidiagonal t p).Finite

Alias of Set.SMulAntidiagonal.finite_of_finite_fst.

@[deprecated Finset.VAddAntidiagonal (since := "2026-02-13")]

def Finsupp.vaddAntidiagonal {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite) : Finset (G × P)

Alias of Finset.VAddAntidiagonal.

Equations

• @Finsupp.vaddAntidiagonal = @Finset.VAddAntidiagonal

@[deprecated Finset.mem_vaddAntidiagonal (since := "2026-02-13")]

theorem Finsupp.mem_vaddAntidiagonal_iff {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite) {x : G × P} : x ∈ Finset.VAddAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a

Alias of Finset.mem_vaddAntidiagonal.

@[deprecated AddMonoidAlgebra.mem_vaddAntidiagonal_of_addGroup (since := "2026-02-13")]

theorem Finsupp.mem_vaddAntidiagonal_of_addGroup {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [AddGroup G] [AddAction G P] [Semiring R] [Zero V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) (gh : G × P) : gh ∈ Finset.VAddAntidiagonal p ⋯ ↔ f gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = -gh.1 +ᵥ p

Alias of AddMonoidAlgebra.mem_vaddAntidiagonal_of_addGroup.

@[deprecated AddMonoidAlgebra.smul_eq (since := "2026-02-13")]

theorem Finsupp.smul_eq {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [VAdd G P] [IsLeftCancelVAdd G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) (hp : ((↑f.support).vaddAntidiagonal (Function.support x) p).Finite := ⋯) : (f • x) p = ∑ gh ∈ Finset.VAddAntidiagonal p hp, f gh.1 • x gh.2

Alias of AddMonoidAlgebra.smul_eq.

@[deprecated AddMonoidAlgebra.smul_apply_addAction (since := "2026-02-13")]

theorem Finsupp.smul_apply_addAction {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [AddGroup G] [AddAction G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) : (f • x) p = ∑ i ∈ f.support, f i • x (-i +ᵥ p)

Alias of AddMonoidAlgebra.smul_apply_addAction.