Commit 2024-03-04 07:58 2e87ddab

View on Github →

chore: Rename lemmas about the coercion List → Multiset (#11099) These did not respect the naming convention by having the coe as a prefix instead of a suffix, or vice-versa. Also add a bunch of norm_cast

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Algebra/BigOperators/Multiset/Basic.lean

deleted theorem Multiset.coe_prod

added theorem Multiset.prod_coe

Modified Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Combinatorics/Partition.lean

Modified Mathlib/Data/Finsupp/BigOperators.lean

Modified Mathlib/Data/Multiset/Antidiagonal.lean

Modified Mathlib/Data/Multiset/Basic.lean

deleted theorem Multiset.coe_filter

deleted theorem Multiset.coe_filterMap

deleted theorem Multiset.coe_map

added theorem Multiset.filterMap_coe

added theorem Multiset.filter_coe

added theorem Multiset.map_coe

Modified Mathlib/Data/Multiset/Bind.lean

Modified Mathlib/Data/Multiset/Functor.lean

Modified Mathlib/Data/Multiset/NatAntidiagonal.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/MvPolynomial/Variables.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/PNat/Factors.lean

Modified Mathlib/Data/Polynomial/RingDivision.lean

Modified Mathlib/Data/Set/Pointwise/BigOperators.lean

Modified Mathlib/Deprecated/Submonoid.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified Mathlib/Logic/Equiv/List.lean

Modified Mathlib/Order/Height.lean

Modified Mathlib/RingTheory/Int/Basic.lean