Commit 2024-09-28 11:27 06eff6ae

View on Github →

chore(Multilinear): golf (#17198) Also add 2 missing simp lemmas

Estimated changes

Modified Mathlib/Data/Finset/Pi.lean

added theorem Finset.pi_eq_empty

Modified Mathlib/Data/Fintype/Pi.lean

modified theorem Fintype.piFinset_empty

added theorem Fintype.piFinset_eq_empty

modified theorem Fintype.piFinset_nonempty

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean