Theorem Finset.HasMulAntidiagonal.nonempty_antidiagonal

Modification history

2026-08-25 13:18
Mathlib/Algebra/Order/Antidiag/Prod.lean
chore(Algebra/Order/Antidiag): relax an assumption in the definition of `HasAntidiagonal` (#41521) …
Modified Finset.HasMulAntidiagonal.nonempty_antidiagonalView on Github →
2026-06-29 09:26
Mathlib/Algebra/Order/Antidiag/Prod.lean
feat: define multivariate restricted power series (#32692) …
Added Finset.HasMulAntidiagonal.nonempty_antidiagonalView on Github →