Commit 2026-08-27 06:58 25578294

View on Github →

chore: card -> length for List.length in names (#43155) Some theorem names used card instead of length to refer to List.length.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/List/Defs.lean

deleted theorem List.prod_eq_pow_card

added theorem List.prod_eq_pow_length

Modified Mathlib/Algebra/Order/BigOperators/Group/List.lean

deleted theorem List.pow_card_le_prod

added theorem List.pow_length_le_prod

deleted theorem List.prod_le_pow_card

added theorem List.prod_le_pow_length

Modified Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

Modified Mathlib/Algebra/TrivSqZeroExt/Basic.lean

Modified Mathlib/Data/Finset/NoncommProd.lean