Theorem IncidenceAlgebra.prod_mul_prod'

Modification history

2025-03-17 06:31

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

chore: Migrate to `DecidableLT` and `DecidableLE` (#22238) …

Modified IncidenceAlgebra.prod_mul_prod'View on Github →

2024-12-11 04:11

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

chore: used named arguments instead of @DecidableRel (#19850)

Modified IncidenceAlgebra.prod_mul_prod'View on Github →

2024-11-11 17:57

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

feat: Incidence algebras (#8900) …

Added IncidenceAlgebra.prod_mul_prod'View on Github →