Theorem Finset.Nonempty.piFinset_const

Modification history

2024-08-01 16:02

Mathlib/Data/Fintype/Pi.lean

chore: backports for leanprover/lean4#4814 (part 9) (#15389) …

Modified Finset.Nonempty.piFinset_const View on Github →

2024-07-31 05:14

Mathlib/Data/Fintype/Pi.lean

feat: Lemmas specialised to `piFinset fun _ : Fin n ↦ s` (#15329) …

Added Finset.Nonempty.piFinset_const View on Github →