Commit 2023-01-30 20:12 c73daed2

View on Github →

chore: fix naming in GroupTheory.Submonoid.Membership (#1950) As seen in #1864, but I was too slow.

Estimated changes

Modified Mathlib/GroupTheory/Subgroup/Finite.lean

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

added theorem Submonoid.multiset_noncommProd_mem

deleted theorem Submonoid.multiset_noncomm_prod_mem

added theorem Submonoid.noncommProd_mem

deleted theorem Submonoid.noncomm_prod_mem