Commit 2026-08-25 13:18 bfc23088

View on Github →

chore(Algebra/Order/Antidiag): relax an assumption in the definition of HasAntidiagonal (#41521) This PR relaxes the typeclass requirement for HasAntidiagonal from AddMonoid A to Add A, which is useful for defining multiplications in TotalMonoidAlgebra(#41472).

Estimated changes

Modified Mathlib/Algebra/Order/Antidiag/Prod.lean

modified theorem Finset.HasMulAntidiagonal.congr

modified theorem Finset.HasMulAntidiagonal.map_prodComm_mulAntidiagonal

modified theorem Finset.HasMulAntidiagonal.map_swap_mulAntidiagonal

modified theorem Finset.HasMulAntidiagonal.nonempty_antidiagonal

modified def Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd

modified theorem Finset.HasMulAntidiagonal.swap_mem_mulAntidiagonal

Modified Mathlib/Algebra/Order/Antidiag/Tendsto.lean