Theorem Finset.HasMulAntidiagonal.map_prodComm_mulAntidiagonal

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.map_prodComm_mulAntidiagonalView on Github →
2026-06-25 19:06
Mathlib/Algebra/Order/Antidiag/Prod.lean
feat(Algebra/Order/Antidiag/Prod): add HasMulAntidiagonal (#38623) …
Added Finset.HasMulAntidiagonal.map_prodComm_mulAntidiagonalView on Github →