Commit 2025-03-27 07:33 85a72d83

View on Github →

chore: some erw in MvPolynomial/Rename (#23355)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Data/Finset/Defs.lean

modified theorem Finset.mem_val

Modified Mathlib/Data/Set/CoeSort.lean

added theorem Set.elem_mem